Documentation
Mathlib
.
GroupTheory
.
Subsemigroup
.
Lemmas
Search
return to top
source
Imports
Init
Mathlib.GroupTheory.Subsemigroup.Center
Mathlib.Algebra.Group.Subsemigroup.Operations
Imported by
Subsemigroup
.
center_prod
AddSubsemigroup
.
center_sum
Lemmas about subsemigroups
#
This file collects various lemmas about subsemigroups.
source
theorem
Subsemigroup
.
center_prod
{
M
:
Type
u_1}
{
N
:
Type
u_2}
[
Mul
M
]
[
Mul
N
]
:
center
(
M
×
N
)
=
(
center
M
)
.
prod
(
center
N
)
source
theorem
AddSubsemigroup
.
center_sum
{
M
:
Type
u_1}
{
N
:
Type
u_2}
[
Add
M
]
[
Add
N
]
:
center
(
M
×
N
)
=
(
center
M
)
.
prod
(
center
N
)