# Centralizers of subgroups #

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

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

Equations
• = { carrier := s.addCentralizer, add_mem' := , zero_mem' := , neg_mem' := }
Instances For
def Subgroup.centralizer {G : Type u_1} [] (s : Set G) :

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

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