# Documentation

Mathlib.GroupTheory.Subsemigroup.Centralizer

# Centralizers of magmas and semigroups #

## Main definitions #

• Set.centralizer: the centralizer of a subset of a magma
• Subsemigroup.centralizer: the centralizer of a subset of a semigroup
• Set.addCentralizer: the centralizer of a subset of an additive magma
• 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) [inst : Add M] :
Set M

The centralizer of a subset of an additive magma.

Equations
• = { c | ∀ (m : M), m Sm + c = c + m }
def Set.centralizer {M : Type u_1} (S : Set M) [inst : Mul M] :
Set M

The centralizer of a subset of a magma.

Equations
• = { c | ∀ (m : M), m Sm * c = c * m }
theorem Set.mem_add_centralizer {M : Type u_1} {S : Set M} [inst : Add M] {c : M} :
∀ (m : M), m Sm + c = c + m
theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : Mul M] {c : M} :
∀ (m : M), m Sm * c = c * m
instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [inst : Add M] [inst : (a : M) → Decidable (∀ (b : M), b Sb + a = a + b)] :
DecidablePred fun x =>
Equations
instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : Mul M] [inst : (a : M) → Decidable (∀ (b : M), b Sb * a = a * b)] :
DecidablePred fun x =>
Equations
@[simp]
theorem Set.zero_mem_add_centralizer {M : Type u_1} (S : Set M) [inst : ] :
@[simp]
theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [inst : ] :
@[simp]
theorem Set.zero_mem_centralizer {M : Type u_1} (S : Set M) [inst : ] :
@[simp]
theorem Set.add_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a + b
@[simp]
theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a * b
@[simp]
theorem Set.neg_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : ] (ha : ) :
@[simp]
theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : ] (ha : ) :
@[simp]
theorem Set.add_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a + b
@[simp]
theorem Set.neg_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : Mul M] [inst : ] (ha : ) :
@[simp]
theorem Set.inv_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} [inst : ] (ha : ) :
@[simp]
theorem Set.sub_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a - b
@[simp]
theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a / b
@[simp]
theorem Set.div_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : ] (ha : ) (hb : ) :
a / b
theorem Set.add_centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [inst : Add M] (h : S T) :
theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [inst : Mul M] (h : S T) :
@[simp]
@[simp]
theorem Set.centralizer_univ (M : Type u_1) [inst : Mul M] :
Set.centralizer Set.univ =
@[simp]
theorem Set.add_centralizer_eq_univ {M : Type u_1} (S : Set M) [inst : ] :
= Set.univ
@[simp]
theorem Set.centralizer_eq_univ {M : Type u_1} (S : Set M) [inst : ] :
= Set.univ
def AddSubsemigroup.centralizer {M : Type u_1} (S : Set M) [inst : ] :

The centralizer of a subset of an additive semigroup.

Equations
• = { carrier := , add_mem' := (_ : ∀ {a b : M}, a + b ) }
def AddSubsemigroup.centralizer.proof_1 {M : Type u_1} (S : Set M) [inst : ] :
∀ {a b : M}, a + b
Equations
• (_ : a + b ) = (_ : a + b )
def Subsemigroup.centralizer {M : Type u_1} (S : Set M) [inst : ] :

The centralizer of a subset of a semigroup M.

Equations
• = { carrier := , mul_mem' := (_ : ∀ {a b : M}, a * b ) }
@[simp]
theorem AddSubsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [inst : ] :
@[simp]
theorem Subsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [inst : ] :
theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : ] {z : M} :
∀ (g : M), g Sg + z = z + g
theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : ] {z : M} :
∀ (g : M), g Sg * z = z * g
instance AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b Sb + a = a + b)] :
Equations
instance Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : ] (a : M) [inst : Decidable (∀ (b : M), b Sb * a = a * b)] :
Equations
theorem AddSubsemigroup.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [inst : ] (h : S T) :
theorem Subsemigroup.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [inst : ] (h : S T) :
@[simp]
theorem AddSubsemigroup.centralizer_univ (M : Type u_1) [inst : ] :
@[simp]
theorem Subsemigroup.centralizer_univ (M : Type u_1) [inst : ] :