Documentation
MeanFourier
.
Mathlib
.
Algebra
.
Group
.
Pointwise
.
Set
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Pi.Basic
Mathlib.Algebra.Group.Pointwise.Set.Basic
Imported by
Set
.
pi_mul
Set
.
pi_add
Set
.
pi_pow
Set
.
nsmul_pi
Set
.
univ_pi_pow
Set
.
nsmul_univ_pi
source
theorem
Set
.
pi_mul
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
Monoid
(
M
i
)
]
(
s
:
Set
ι
)
(
t
u
:
(
i
:
ι
) →
Set
(
M
i
)
)
:
(
s
.
pi
fun (
i
:
ι
) =>
t
i
*
u
i
)
=
s
.
pi
t
*
s
.
pi
u
source
theorem
Set
.
pi_add
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
AddMonoid
(
M
i
)
]
(
s
:
Set
ι
)
(
t
u
:
(
i
:
ι
) →
Set
(
M
i
)
)
:
(
s
.
pi
fun (
i
:
ι
) =>
t
i
+
u
i
)
=
s
.
pi
t
+
s
.
pi
u
source
theorem
Set
.
pi_pow
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
Monoid
(
M
i
)
]
(
s
:
Set
ι
)
(
t
:
(
i
:
ι
) →
Set
(
M
i
)
)
{
n
:
ℕ
}
:
n
≠
0
→
s
.
pi
t
^
n
=
s
.
pi
fun (
i
:
ι
) =>
t
i
^
n
source
theorem
Set
.
nsmul_pi
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
AddMonoid
(
M
i
)
]
(
s
:
Set
ι
)
(
t
:
(
i
:
ι
) →
Set
(
M
i
)
)
{
n
:
ℕ
}
:
n
≠
0
→
n
•
s
.
pi
t
=
s
.
pi
fun (
i
:
ι
) =>
n
•
t
i
source
theorem
Set
.
univ_pi_pow
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
Monoid
(
M
i
)
]
(
t
:
(
i
:
ι
) →
Set
(
M
i
)
)
(
n
:
ℕ
)
:
univ
.
pi
t
^
n
=
univ
.
pi
fun (
i
:
ι
) =>
t
i
^
n
source
theorem
Set
.
nsmul_univ_pi
{
ι
:
Type
u_1}
{
M
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
AddMonoid
(
M
i
)
]
(
t
:
(
i
:
ι
) →
Set
(
M
i
)
)
(
n
:
ℕ
)
:
n
•
univ
.
pi
t
=
univ
.
pi
fun (
i
:
ι
) =>
n
•
t
i