# 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) [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubmonoid.center.proof_2 (M : Type u_1) [inst : ] :
Equations
• (_ : ) = (_ : )
def AddSubmonoid.center.proof_1 (M : Type u_1) [inst : ] :
∀ {a b : M}, a + b
Equations
• (_ : a + b ) = (_ : a + b )
def Submonoid.center (M : Type u_1) [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
theorem AddSubmonoid.coe_center (M : Type u_1) [inst : ] :
theorem Submonoid.coe_center (M : Type u_1) [inst : ] :
↑() =
@[simp]
@[simp]
theorem Submonoid.center_toSubsemigroup (M : Type u_1) [inst : ] :
().toSubsemigroup =
theorem AddSubmonoid.mem_center_iff {M : Type u_1} [inst : ] {z : M} :
∀ (g : M), g + z = z + g
theorem Submonoid.mem_center_iff {M : Type u_1} [inst : ] {z : M} :
∀ (g : M), g * z = z * g
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Submonoid.decidableMemCenter {M : Type u_1} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b * a = a * b)] :
Equations
instance Submonoid.center.commMonoid {M : Type u_1} [inst : ] :
CommMonoid { x // }

The center of a monoid is commutative.

Equations
• Submonoid.center.commMonoid = let src := ; CommMonoid.mk (_ : ∀ (x b : { x // }), x * b = b * x)
instance Submonoid.center.smulCommClass_left {M : Type u_1} [inst : ] :
SMulCommClass { x // } M M

The center of a monoid acts commutatively on that monoid.

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

The center of a monoid acts commutatively on that monoid.

Equations

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) [inst : ] :