Documentation
Monlib
.
Preq
.
Set
Search
return to top
source
Imports
Init
Mathlib.Tactic.NthRewrite
Mathlib.Algebra.Group.Prod
Mathlib.GroupTheory.Subsemigroup.Center
Imported by
Set
.
center_prod
Set
.
center_pi
source
theorem
Set
.
center_prod
{
A
:
Type
u_1}
{
B
:
Type
u_2}
[
Semigroup
A
]
[
Semigroup
B
]
:
center
(
A
×
B
)
=
center
A
×ˢ
center
B
source
theorem
Set
.
center_pi
{
ι
:
Type
u_1}
{
A
:
ι
→
Type
u_2
}
[
(
i
:
ι
) →
Semigroup
(
A
i
)
]
[
DecidableEq
ι
]
:
center
((
i
:
ι
) →
A
i
)
=
univ
.
pi
fun (
i
:
ι
) =>
center
(
A
i
)