Documentation

Mathlib.GroupTheory.Subsemigroup.Centralizer

Centralizers in semigroups, as subsemigroups. #

Main definitions #

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

The centralizer of a subset of an additive semigroup.

Equations
Instances For

    The centralizer of a subset of a semigroup M.

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