Documentation

Mathlib.GroupTheory.Subgroup.Centralizer

Centralizers of subgroups #

theorem AddSubgroup.centralizer.proof_1 {G : Type u_1} [AddGroup G] (s : Set G) :
∀ {a b : G}, a (AddSubmonoid.centralizer s).carrierb (AddSubmonoid.centralizer s).carriera + b (AddSubmonoid.centralizer s).carrier
def AddSubgroup.centralizer {G : Type u_1} [AddGroup G] (s : Set G) :

The centralizer of H is the additive subgroup of g : G commuting with every h : H.

Equations
Instances For
    def Subgroup.centralizer {G : Type u_1} [Group G] (s : Set G) :

    The centralizer of H is the subgroup of g : G commuting with every h : H.

    Equations
    Instances For
      theorem AddSubgroup.mem_centralizer_iff {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
      g AddSubgroup.centralizer s hs, h + g = g + h
      theorem Subgroup.mem_centralizer_iff {G : Type u_1} [Group G] {g : G} {s : Set G} :
      g Subgroup.centralizer s hs, h * g = g * h
      theorem AddSubgroup.mem_centralizer_iff_commutator_eq_zero {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
      g AddSubgroup.centralizer s hs, h + g + -h + -g = 0
      theorem Subgroup.mem_centralizer_iff_commutator_eq_one {G : Type u_1} [Group G] {g : G} {s : Set G} :
      g Subgroup.centralizer s hs, h * g * h⁻¹ * g⁻¹ = 1
      theorem Subgroup.centralizer_le {G : Type u_1} [Group G] {s : Set G} {t : Set G} (h : s t) :
      instance AddSubgroup.Centralizer.characteristic {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic] :
      (AddSubgroup.centralizer H).Characteristic
      Equations
      • =
      instance Subgroup.Centralizer.characteristic {G : Type u_1} [Group G] {H : Subgroup G} [hH : H.Characteristic] :
      (Subgroup.centralizer H).Characteristic
      Equations
      • =
      theorem Subgroup.le_centralizer_iff_isCommutative {G : Type u_1} [Group G] {K : Subgroup G} :
      K Subgroup.centralizer K K.IsCommutative
      theorem AddSubgroup.le_centralizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] :
      theorem Subgroup.le_centralizer {G : Type u_1} [Group G] (H : Subgroup G) [h : H.IsCommutative] :