# Centralizers of magmas and semigroups #

## Main definitions #

• Set.centralizer: the centralizer of a subset of a magma
• Set.addCentralizer: the centralizer of a subset of an additive magma

See Mathlib.GroupTheory.Subsemigroup.Centralizer for the definition of the centralizer as a subsemigroup:

• 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 Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :
Set M

The centralizer of a subset of an additive magma.

Equations
• S.addCentralizer = {c : M | mS, m + c = c + m}
Instances For
def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :
Set M

The centralizer of a subset of a magma.

Equations
• S.centralizer = {c : M | mS, m * c = c * m}
Instances For
theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :
c S.addCentralizer mS, m + c = c + m
theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :
c S.centralizer mS, m * c = c * m
instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [Add M] [(a : M) → Decidable (bS, b + a = a + b)] :
DecidablePred fun (x : M) => x S.addCentralizer
Equations
instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (bS, b * a = a * b)] :
DecidablePred fun (x : M) => x S.centralizer
Equations
@[simp]
theorem Set.zero_mem_addCentralizer {M : Type u_1} (S : Set M) [] :
@[simp]
theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [] :
1 S.centralizer
@[simp]
theorem Set.zero_mem_centralizer {M : Type u_1} (S : Set M) [] :
0 S.centralizer
@[simp]
theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [] (ha : a S.addCentralizer) (hb : b S.addCentralizer) :
@[simp]
theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [] (ha : a S.centralizer) (hb : b S.centralizer) :
a * b S.centralizer
@[simp]
theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} [] (ha : a S.addCentralizer) :
@[simp]
theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [] (ha : a S.centralizer) :
a⁻¹ S.centralizer
@[simp]
theorem Set.inv_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} [] (ha : a S.centralizer) :
a⁻¹ S.centralizer
@[simp]
theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [] (ha : a S.addCentralizer) (hb : b S.addCentralizer) :
@[simp]
theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [] (ha : a S.centralizer) (hb : b S.centralizer) :
a / b S.centralizer
@[simp]
theorem Set.div_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} {b : M} [] (ha : a S.centralizer) (hb : b S.centralizer) :
a / b S.centralizer
theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S T) :
theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S T) :
T.centralizer S.centralizer
theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) :
S.centralizer
@[simp]
theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [] :
@[simp]
theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [] :
s.centralizer = Set.univ s
@[simp]
theorem Set.addCentralizer_univ (M : Type u_1) [] :