mathlib documentation

group_theory.subsemigroup.centralizer

Centralizers of magmas and semigroups #

Main definitions #

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} :
c S.add_centralizer ∀ (m : M), m Sm + 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 Sm * c = c * m
@[protected, instance]
def set.decidable_mem_add_centralizer {M : Type u_1} {S : set M} [has_add M] [decidable_eq M] [fintype M] [decidable_pred (λ (_x : M), _x S)] :
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] [decidable_eq M] [fintype M] [decidable_pred (λ (_x : M), _x S)] :
decidable_pred (λ (_x : M), _x S.centralizer)
Equations
@[simp]
theorem set.zero_mem_add_centralizer {M : Type u_1} (S : set M) [add_zero_class M] :
@[simp]
theorem set.one_mem_centralizer {M : Type u_1} (S : set M) [mul_one_class M] :
@[simp]
theorem set.zero_mem_centralizer {M : Type u_1} (S : set M) [mul_zero_class 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} [add_semigroup 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] [has_distrib_neg M] (ha : a S.centralizer) :
@[simp]
theorem set.inv_mem_centralizer₀ {M : Type u_1} {S : set M} {a : M} [group_with_zero 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} [group_with_zero 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) :
@[simp]
theorem set.centralizer_univ (M : Type u_1) [has_mul M] :
@[simp]
@[simp]
theorem set.centralizer_eq_univ {M : Type u_1} (S : set M) [comm_semigroup 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) [add_semigroup M] :

The centralizer of a subset of an additive semigroup.

Equations
@[simp, norm_cast]
@[simp, norm_cast]
theorem subsemigroup.mem_centralizer_iff {M : Type u_1} {S : set M} [semigroup M] {z : M} :
z subsemigroup.centralizer S ∀ (g : M), g Sg * z = z * g
theorem add_subsemigroup.mem_centralizer_iff {M : Type u_1} {S : set M} [add_semigroup M] {z : M} :
z add_subsemigroup.centralizer S ∀ (g : M), g Sg + z = z + g
@[protected, instance]
def subsemigroup.decidable_mem_centralizer {M : Type u_1} {S : set M} [semigroup M] [decidable_eq M] [fintype M] [decidable_pred (λ (_x : M), _x S)] :
Equations
@[protected, instance]
def add_subsemigroup.decidable_mem_centralizer {M : Type u_1} {S : set M} [add_semigroup M] [decidable_eq M] [fintype M] [decidable_pred (λ (_x : M), _x S)] :
Equations