# Documentation

Mathlib.GroupTheory.Submonoid.Center

# Centers of monoids #

## Main definitions #

• Submonoid.center: the center of a monoid
• AddSubmonoid.center: the center of an additive monoid

We provide Subgroup.center, AddSubgroup.center, Subsemiring.center, and Subring.center in other files.

def AddSubmonoid.center (M : Type u_1) [] :

The center of a monoid M is the set of elements that commute with everything in M

Instances For
theorem AddSubmonoid.center.proof_1 (M : Type u_1) [] :
∀ {a b : M}, a + b
def Submonoid.center (M : Type u_1) [] :

The center of a monoid M is the set of elements that commute with everything in M

Instances For
theorem AddSubmonoid.coe_center (M : Type u_1) [] :
theorem Submonoid.coe_center (M : Type u_1) [] :
↑() =
@[simp]
@[simp]
theorem Submonoid.center_toSubsemigroup (M : Type u_1) [] :
().toSubsemigroup =
theorem AddSubmonoid.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g + z = z + g
theorem Submonoid.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g * z = z * g
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
instance Submonoid.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
instance Submonoid.center.commMonoid {M : Type u_1} [] :
CommMonoid { x // }

The center of a monoid is commutative.

instance Submonoid.center.smulCommClass_left {M : Type u_1} [] :
SMulCommClass { x // } M M

The center of a monoid acts commutatively on that monoid.

instance Submonoid.center.smulCommClass_right {M : Type u_1} [] :
SMulCommClass M { x // } M

The center of a monoid acts commutatively on that monoid.

Note that smulCommClass (center M) (center M) M is already implied by Submonoid.smulCommClass_right

@[simp]
theorem Submonoid.center_eq_top (M : Type u_1) [] :
theorem addUnitsCenterToCenterAddUnits.proof_2 (M : Type u_1) [] (u : AddUnits { x // }) (r : ) :
r + = + r
AddUnits { x // } →+ { x // }

For an additive monoid, the units of the center inject into the center of the units.

Instances For
@[simp]
For a monoid, the units of the center inject into the center of the units. This is not an equivalence in general; one case when it is is for groups with zero, which is covered in centerUnitsEquivUnitsCenter.