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

The centralizer of a subset of a semigroup M.

Equations
@[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