Documentation

Mathlib.GroupTheory.Submonoid.Centralizer

Centralizers of magmas and monoids #

Main definitions #

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

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

The centralizer of a subset of an additive monoid.

Equations
  • One or more equations did not get rendered due to their size.
def Submonoid.centralizer {M : Type u_1} (S : Set M) [inst : Monoid M] :

The centralizer of a subset of a monoid M.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [inst : Monoid M] :
theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : AddMonoid M] {z : M} :
z AddSubmonoid.centralizer S ∀ (g : M), g Sg + z = z + g
theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : Monoid M] {z : M} :
z Submonoid.centralizer S ∀ (g : M), g Sg * z = z * g
instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : AddMonoid M] (a : M) [inst : Decidable (∀ (b : M), b Sb + a = a + b)] :
Equations
instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : Monoid M] (a : M) [inst : Decidable (∀ (b : M), b Sb * a = a * b)] :
Equations
theorem Submonoid.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [inst : Monoid M] (h : S T) :