# mathlib3documentation

group_theory.submonoid.centralizer

# Centralizers of magmas and monoids #

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

## Main definitions #

• submonoid.centralizer: the centralizer of a subset of a monoid
• add_submonoid.centralizer: the centralizer of a subset of an additive monoid

We provide subgroup.centralizer, add_subgroup.centralizer in other files.

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

The centralizer of a subset of a monoid M.

Equations
def add_submonoid.centralizer {M : Type u_1} (S : set M) [add_monoid M] :

The centralizer of a subset of an additive monoid.

Equations
@[simp, norm_cast]
theorem add_submonoid.coe_centralizer {M : Type u_1} (S : set M) [add_monoid M] :
@[simp, norm_cast]
theorem submonoid.coe_centralizer {M : Type u_1} (S : set M) [monoid M] :
theorem submonoid.centralizer_to_subsemigroup {M : Type u_1} (S : set M) [monoid M] :
theorem submonoid.mem_centralizer_iff {M : Type u_1} {S : set M} [monoid M] {z : M} :
(g : M), g S g * z = z * g
theorem add_submonoid.mem_centralizer_iff {M : Type u_1} {S : set M} [add_monoid M] {z : M} :
(g : M), g S g + z = z + g
theorem submonoid.center_le_centralizer {M : Type u_1} [monoid M] (s : set M) :
theorem add_submonoid.center_le_centralizer {M : Type u_1} [add_monoid M] (s : set M) :
@[protected, instance]
def submonoid.decidable_mem_centralizer {M : Type u_1} {S : set M} [monoid M] (a : M) [decidable ( (b : M), b S b * a = a * b)] :
Equations
@[protected, instance]
def add_submonoid.decidable_mem_centralizer {M : Type u_1} {S : set M} [add_monoid M] (a : M) [decidable ( (b : M), b S b + a = a + b)] :
Equations
theorem add_submonoid.centralizer_le {M : Type u_1} {S T : set M} [add_monoid M] (h : S T) :
theorem submonoid.centralizer_le {M : Type u_1} {S T : set M} [monoid M] (h : S T) :
@[simp]
@[simp]
theorem submonoid.centralizer_eq_top_iff_subset {M : Type u_1} [monoid M] {s : set M} :
s
@[simp]
theorem submonoid.centralizer_univ (M : Type u_1) [monoid M] :
@[simp]