Documentation

Mathlib.GroupTheory.Submonoid.Centralizer

Centralizers of magmas and monoids #

Main definitions #

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

The centralizer of a subset of an additive monoid.

Equations
Instances For
    def Submonoid.centralizer {M : Type u_1} (S : Set M) [Monoid M] :

    The centralizer of a subset of a monoid M.

    Equations
    Instances For
      @[simp]
      theorem AddSubmonoid.coe_centralizer {M : Type u_1} (S : Set M) [AddMonoid M] :
      (AddSubmonoid.centralizer S) = S.addCentralizer
      @[simp]
      theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [Monoid M] :
      (Submonoid.centralizer S) = S.centralizer
      theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddMonoid M] {z : M} :
      z AddSubmonoid.centralizer S gS, g + z = z + g
      theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [Monoid M] {z : M} :
      z Submonoid.centralizer S gS, g * z = z * g
      instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddMonoid M] (a : M) [Decidable (∀ bS, b + a = a + b)] :
      Equations
      instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [Monoid M] (a : M) [Decidable (∀ bS, b * a = a * b)] :
      Equations
      @[simp]