# mathlibdocumentation

group_theory.submonoid.center

# Centers of monoids #

## Main definitions #

• submonoid.center: the center of a monoid
• add_submonoid.center: the center of an additive monoid

We provide subgroup.center, add_subgroup.center, subsemiring.center, and subring.center in other files.

def submonoid.center (M : Type u_1) [monoid M] :

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

Equations
Instances for ↥submonoid.center
def add_submonoid.center (M : Type u_1) [add_monoid M] :

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

Equations
theorem add_submonoid.coe_center (M : Type u_1) [add_monoid M] :
theorem submonoid.coe_center (M : Type u_1) [monoid M] :
@[simp]
theorem submonoid.center_to_subsemigroup (M : Type u_1) [monoid M] :
theorem add_submonoid.mem_center_iff {M : Type u_1} [add_monoid M] {z : M} :
∀ (g : M), g + z = z + g
theorem submonoid.mem_center_iff {M : Type u_1} [monoid M] {z : M} :
∀ (g : M), g * z = z * g
@[protected, instance]
def submonoid.decidable_mem_center {M : Type u_1} [monoid M] [decidable_eq M] [fintype M] :
decidable_pred (λ (_x : M), _x submonoid.center M)
Equations
@[protected, instance]
def submonoid.center.comm_monoid {M : Type u_1} [monoid M] :

The center of a monoid is commutative.

Equations
@[protected, instance]
def submonoid.center.smul_comm_class_left {M : Type u_1} [monoid M] :
M

The center of a monoid acts commutatively on that monoid.

@[protected, instance]
def submonoid.center.smul_comm_class_right {M : Type u_1} [monoid M] :
M

The center of a monoid acts commutatively on that monoid.

Note that smul_comm_class (center M) (center M) M is already implied by submonoid.smul_comm_class_right

@[simp]
theorem submonoid.center_eq_top (M : Type u_1) [comm_monoid M] :