Centralizers of subgroups #
The centralizer
of s
is the subgroup of g : G
commuting with every h : s
.
Equations
- Subgroup.centralizer s = { carrier := s.centralizer, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The centralizer
of s
is the additive subgroup of g : G
commuting with every h : s
.
Equations
- AddSubgroup.centralizer s = { carrier := s.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
@[simp]
@[simp]
instance
Subgroup.Centralizer.characteristic
{G : Type u_1}
[Group G]
{H : Subgroup G}
[hH : H.Characteristic]
:
instance
AddSubgroup.Centralizer.characteristic
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
[hH : H.Characteristic]
:
theorem
AddSubgroup.le_centralizer_iff_isCommutative
{G : Type u_1}
[AddGroup G]
{K : AddSubgroup G}
:
theorem
AddSubgroup.le_centralizer
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[h : H.IsCommutative]
:
@[simp]
theorem
Subgroup.instMulDistribMulActionSubtypeMemNormalizer_smul_coe
{G : Type u_1}
[Group G]
(H : Subgroup G)
(g : ↥H.normalizer)
(h : ↥H)
:
The homomorphism N(H) → Aut(H) with kernel C(H).
Instances For
@[simp]
theorem
Subgroup.normalizerMonoidHom_apply_apply_coe
{G : Type u_1}
[Group G]
(H : Subgroup G)
(x : ↥H.normalizer)
(a✝ : ↥H)
: