# Centralizers of magmas and monoids #

## Main definitions #

• Submonoid.centralizer: the centralizer of a subset of a monoid
• AddSubmonoid.centralizer: the centralizer of a subset of an additive monoid

We provide Subgroup.centralizer, AddSubgroup.centralizer in other files.

theorem AddSubmonoid.centralizer.proof_2 {M : Type u_1} (S : Set M) [] :
def AddSubmonoid.centralizer {M : Type u_1} (S : Set M) [] :

The centralizer of a subset of an additive monoid.

Equations
• = { carrier := S.addCentralizer, add_mem' := , zero_mem' := }
Instances For
theorem AddSubmonoid.centralizer.proof_1 {M : Type u_1} (S : Set M) [] :
def Submonoid.centralizer {M : Type u_1} (S : Set M) [] :

The centralizer of a subset of a monoid M.

Equations
• = { carrier := S.centralizer, mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem AddSubmonoid.coe_centralizer {M : Type u_1} (S : Set M) [] :
@[simp]
theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [] :
= S.centralizer
theorem Submonoid.centralizer_toSubsemigroup {M : Type u_1} (S : Set M) [] :
.toSubsemigroup =
theorem AddSubmonoid.centralizer_toAddSubsemigroup {M : Type u_2} [] (S : Set M) :
theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [] {z : M} :
gS, g + z = z + g
theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [] {z : M} :
gS, g * z = z * g
theorem AddSubmonoid.center_le_centralizer {M : Type u_1} [] (s : Set M) :
theorem Submonoid.center_le_centralizer {M : Type u_1} [] (s : Set M) :
instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [] (a : M) [Decidable (bS, b + a = a + b)] :
Equations
instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [] (a : M) [Decidable (bS, b * a = a * b)] :
Equations
theorem AddSubmonoid.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [] (h : S T) :
theorem Submonoid.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [] (h : S T) :
@[simp]
theorem AddSubmonoid.centralizer_eq_top_iff_subset {M : Type u_1} [] {s : Set M} :
s
@[simp]
theorem Submonoid.centralizer_eq_top_iff_subset {M : Type u_1} [] {s : Set M} :
s ()
@[simp]
@[simp]
theorem Submonoid.centralizer_univ (M : Type u_1) [] :
theorem Submonoid.le_centralizer_centralizer (M : Type u_1) [] {s : } :
@[simp]
theorem AddSubmonoid.centralizer_centralizer_centralizer (M : Type u_1) [] {s : Set M} :