# mathlib3documentation

group_theory.subsemigroup.centralizer

# Centralizers of magmas and semigroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• set.centralizer: the centralizer of a subset of a magma
• subsemigroup.centralizer: the centralizer of a subset of a semigroup
• set.add_centralizer: the centralizer of a subset of an additive magma
• add_subsemigroup.centralizer: the centralizer of a subset of an additive semigroup

We provide monoid.centralizer, add_monoid.centralizer, subgroup.centralizer, and add_subgroup.centralizer in other files.

def set.centralizer {M : Type u_1} (S : set M) [has_mul M] :
set M

The centralizer of a subset of a magma.

Equations
def set.add_centralizer {M : Type u_1} (S : set M) [has_add M] :
set M

The centralizer of a subset of an additive magma.

Equations
theorem set.mem_add_centralizer {M : Type u_1} {S : set M} [has_add M] {c : M} :
(m : M), m S m + c = c + m
theorem set.mem_centralizer_iff {M : Type u_1} {S : set M} [has_mul M] {c : M} :
c S.centralizer (m : M), m S m * c = c * m
@[protected, instance]
def set.decidable_mem_add_centralizer {M : Type u_1} {S : set M} [has_add M] [Π (a : M), decidable ( (b : M), b S b + a = a + b)] :
decidable_pred (λ (_x : M), _x S.add_centralizer)
Equations
@[protected, instance]
def set.decidable_mem_centralizer {M : Type u_1} {S : set M} [has_mul M] [Π (a : M), decidable ( (b : M), b S b * a = a * b)] :
decidable_pred (λ (_x : M), _x S.centralizer)
Equations
@[simp]
theorem set.zero_mem_add_centralizer {M : Type u_1} (S : set M)  :
@[simp]
theorem set.one_mem_centralizer {M : Type u_1} (S : set M)  :
@[simp]
theorem set.zero_mem_centralizer {M : Type u_1} (S : set M)  :
@[simp]
theorem set.mul_mem_centralizer {M : Type u_1} {S : set M} {a b : M} [semigroup M] (ha : a S.centralizer) (hb : b S.centralizer) :
@[simp]
theorem set.add_mem_add_centralizer {M : Type u_1} {S : set M} {a b : M} (ha : a S.add_centralizer) (hb : b S.add_centralizer) :
@[simp]
theorem set.inv_mem_centralizer {M : Type u_1} {S : set M} {a : M} [group M] (ha : a S.centralizer) :
@[simp]
theorem set.neg_mem_add_centralizer {M : Type u_1} {S : set M} {a : M} [add_group M] (ha : a S.add_centralizer) :
@[simp]
theorem set.add_mem_centralizer {M : Type u_1} {S : set M} {a b : M} [distrib M] (ha : a S.centralizer) (hb : b S.centralizer) :
@[simp]
theorem set.neg_mem_centralizer {M : Type u_1} {S : set M} {a : M} [has_mul M] (ha : a S.centralizer) :
@[simp]
theorem set.inv_mem_centralizer₀ {M : Type u_1} {S : set M} {a : M} (ha : a S.centralizer) :
@[simp]
theorem set.div_mem_centralizer {M : Type u_1} {S : set M} {a b : M} [group M] (ha : a S.centralizer) (hb : b S.centralizer) :
@[simp]
theorem set.sub_mem_add_centralizer {M : Type u_1} {S : set M} {a b : M} [add_group M] (ha : a S.add_centralizer) (hb : b S.add_centralizer) :
@[simp]
theorem set.div_mem_centralizer₀ {M : Type u_1} {S : set M} {a b : M} (ha : a S.centralizer) (hb : b S.centralizer) :
theorem set.centralizer_subset {M : Type u_1} {S T : set M} [has_mul M] (h : S T) :
theorem set.add_centralizer_subset {M : Type u_1} {S T : set M} [has_add M] (h : S T) :
theorem set.center_subset_centralizer {M : Type u_1} [has_mul M] (S : set M) :
@[simp]
theorem set.add_centralizer_eq_top_iff_subset {M : Type u_1} {s : set M} [has_add M] :
@[simp]
theorem set.centralizer_eq_top_iff_subset {M : Type u_1} {s : set M} [has_mul M] :
s
@[simp]
@[simp]
theorem set.centralizer_univ (M : Type u_1) [has_mul M] :
@[simp]
theorem set.add_centralizer_eq_univ {M : Type u_1} (S : set M)  :
@[simp]
theorem set.centralizer_eq_univ {M : Type u_1} (S : set M)  :
def subsemigroup.centralizer {M : Type u_1} (S : set M) [semigroup M] :

The centralizer of a subset of a semigroup M.

Equations
def add_subsemigroup.centralizer {M : Type u_1} (S : set M)  :

The centralizer of a subset of an additive semigroup.

Equations
@[simp, norm_cast]
theorem subsemigroup.coe_centralizer {M : Type u_1} (S : set M) [semigroup M] :
@[simp, norm_cast]
theorem add_subsemigroup.coe_centralizer {M : Type u_1} (S : set M)  :
theorem subsemigroup.mem_centralizer_iff {M : Type u_1} {S : set M} [semigroup M] {z : M} :
(g : M), g S g * z = z * g
theorem add_subsemigroup.mem_centralizer_iff {M : Type u_1} {S : set M} {z : M} :
(g : M), g S g + z = z + g
@[protected, instance]
def subsemigroup.decidable_mem_centralizer {M : Type u_1} {S : set M} [semigroup M] (a : M) [decidable ( (b : M), b S b * a = a * b)] :
Equations
@[protected, instance]
def add_subsemigroup.decidable_mem_centralizer {M : Type u_1} {S : set M} (a : M) [decidable ( (b : M), b S b + a = a + b)] :
Equations
theorem add_subsemigroup.center_le_centralizer {M : Type u_1} (S : set M) :
theorem subsemigroup.center_le_centralizer {M : Type u_1} [semigroup M] (S : set M) :
theorem subsemigroup.centralizer_le {M : Type u_1} {S T : set M} [semigroup M] (h : S T) :
theorem add_subsemigroup.centralizer_le {M : Type u_1} {S T : set M} (h : S T) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem subsemigroup.centralizer_univ (M : Type u_1) [semigroup M] :