Documentation
MeanFourier
.
Mathlib
.
Combinatorics
.
Additive
.
CovBySMul
Search
return to top
source
Imports
Init
Mathlib.Combinatorics.Additive.CovBySMul
MeanFourier.Mathlib.Data.Fintype.BigOperators
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.Order.BigOperators.Ring.Finset
Imported by
CovBySMul
.
prod
CovByVAdd
.
sum
CovBySMul
.
pi
CovByVAdd
.
pi
source
theorem
CovBySMul
.
prod
{
G
:
Type
u_1}
[
Group
G
]
{
K
L
:
ℝ
}
{
H
:
Type
u_3}
[
Group
H
]
{
A
B
:
Set
G
}
{
C
D
:
Set
H
}
(
hAB
:
CovBySMul
G
K
A
B
)
(
hCD
:
CovBySMul
H
L
C
D
)
:
CovBySMul
(
G
×
H
) (
K
*
L
) (
A
×ˢ
C
) (
B
×ˢ
D
)
source
theorem
CovByVAdd
.
sum
{
G
:
Type
u_1}
[
AddGroup
G
]
{
K
L
:
ℝ
}
{
H
:
Type
u_3}
[
AddGroup
H
]
{
A
B
:
Set
G
}
{
C
D
:
Set
H
}
(
hAB
:
CovByVAdd
G
K
A
B
)
(
hCD
:
CovByVAdd
H
L
C
D
)
:
CovByVAdd
(
G
×
H
) (
K
*
L
) (
A
×ˢ
C
) (
B
×ˢ
D
)
source
theorem
CovBySMul
.
pi
{
ι
:
Type
u_3}
{
G
:
ι
→
Type
u_4
}
{
X
:
ι
→
Type
u_5
}
{
s
:
Finset
ι
}
[
(
i
:
ι
) →
Group
(
G
i
)
]
[
(
i
:
ι
) →
MulAction
(
G
i
)
(
X
i
)
]
{
A
B
:
(
i
:
ι
) →
Set
(
X
i
)
}
{
K
:
ι
→
ℝ
}
(
hAB
:
∀
i
∈
s
,
CovBySMul
(
G
i
)
(
K
i
)
(
A
i
)
(
B
i
)
)
:
CovBySMul
((
i
:
ι
) →
G
i
)
(∏
i
∈
s
,
K
i
)
(
(↑
s
)
.
pi
A
)
(
(↑
s
)
.
pi
B
)
source
theorem
CovByVAdd
.
pi
{
ι
:
Type
u_3}
{
G
:
ι
→
Type
u_4
}
{
X
:
ι
→
Type
u_5
}
{
s
:
Finset
ι
}
[
(
i
:
ι
) →
AddGroup
(
G
i
)
]
[
(
i
:
ι
) →
AddAction
(
G
i
)
(
X
i
)
]
{
A
B
:
(
i
:
ι
) →
Set
(
X
i
)
}
{
K
:
ι
→
ℝ
}
(
hAB
:
∀
i
∈
s
,
CovByVAdd
(
G
i
)
(
K
i
)
(
A
i
)
(
B
i
)
)
:
CovByVAdd
((
i
:
ι
) →
G
i
)
(∏
i
∈
s
,
K
i
)
(
(↑
s
)
.
pi
A
)
(
(↑
s
)
.
pi
B
)