Documentation

Mathlib.GroupTheory.Subsemigroup.Centralizer

Centralizers of magmas and semigroups #

Main definitions #

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
def Set.centralizer {M : Type u_1} (S : Set M) [inst : Mul M] :
Set M

The centralizer of a subset of a magma.

Equations
theorem Set.mem_add_centralizer {M : Type u_1} {S : Set M} [inst : Add M] {c : M} :
c Set.addCentralizer S ∀ (m : M), m Sm + c = c + m
theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : Mul M] {c : M} :
c Set.centralizer S ∀ (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)] :
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)] :
Equations
@[simp]
theorem Set.zero_mem_add_centralizer {M : Type u_1} (S : Set M) [inst : AddZeroClass M] :
@[simp]
theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [inst : MulOneClass M] :
@[simp]
theorem Set.zero_mem_centralizer {M : Type u_1} (S : Set M) [inst : MulZeroClass M] :
@[simp]
theorem Set.add_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : AddSemigroup M] (ha : a Set.addCentralizer S) (hb : b Set.addCentralizer S) :
@[simp]
theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : Semigroup M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
@[simp]
theorem Set.neg_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : AddGroup M] (ha : a Set.addCentralizer S) :
@[simp]
theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : Group M] (ha : a Set.centralizer S) :
@[simp]
theorem Set.add_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : Distrib M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
@[simp]
theorem Set.neg_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [inst : Mul M] [inst : HasDistribNeg M] (ha : a Set.centralizer S) :
@[simp]
theorem Set.inv_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} [inst : GroupWithZero M] (ha : a Set.centralizer S) :
@[simp]
theorem Set.sub_mem_add_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : AddGroup M] (ha : a Set.addCentralizer S) (hb : b Set.addCentralizer S) :
@[simp]
theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : Group M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
@[simp]
theorem Set.div_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} {b : M} [inst : GroupWithZero M] (ha : a Set.centralizer S) (hb : b Set.centralizer S) :
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]
theorem Set.add_centralizer_univ (M : Type u_1) [inst : Add M] :
@[simp]
theorem Set.centralizer_univ (M : Type u_1) [inst : Mul M] :
@[simp]
theorem Set.add_centralizer_eq_univ {M : Type u_1} (S : Set M) [inst : AddCommSemigroup M] :
@[simp]
theorem Set.centralizer_eq_univ {M : Type u_1} (S : Set M) [inst : CommSemigroup M] :
Set.centralizer S = Set.univ

The centralizer of a subset of an additive semigroup.

Equations
def Subsemigroup.centralizer {M : Type u_1} (S : Set M) [inst : Semigroup M] :

The centralizer of a subset of a semigroup M.

Equations
theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : AddSemigroup M] {z : M} :
z AddSubsemigroup.centralizer S ∀ (g : M), g Sg + z = z + g
theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : Semigroup M] {z : M} :
z Subsemigroup.centralizer S ∀ (g : M), g Sg * z = z * g
instance AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : AddSemigroup M] (a : M) [inst : Decidable (∀ (b : M), b Sb + a = a + b)] :
Equations
instance Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [inst : Semigroup M] (a : M) [inst : Decidable (∀ (b : M), b Sb * a = a * b)] :
Equations