# Centralizers in semigroups, as subsemigroups. #

## Main definitions #

• Subsemigroup.centralizer: the centralizer of a subset of a semigroup
• AddSubsemigroup.centralizer: the centralizer of a subset of an additive semigroup

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

def AddSubsemigroup.centralizer {M : Type u_1} (S : Set M) [] :

The centralizer of a subset of an additive semigroup.

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

The centralizer of a subset of a semigroup M.

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