General commutators. #
If G
is a group and H₁ H₂ : subgroup G
then the general commutator ⁅H₁, H₂⁆ : subgroup G
is the subgroup of G
generated by the commutators h₁ * h₂ * h₁⁻¹ * h₂⁻¹
.
Main definitions #
general_commutator H₁ H₂
: the commutator of the subgroupsH₁
andH₂
@[protected, instance]
The commutator of two subgroups H₁
and H₂
.
theorem
map_general_commutator
{G : Type u_1}
[group G]
{G₂ : Type u_2}
[group G₂]
(f : G →* G₂)
(H₁ H₂ : subgroup G) :
subgroup.map f ⁅H₁,H₂⁆ = ⁅subgroup.map f H₁,subgroup.map f H₂⁆