Commutators of Subgroups #
G is a group and
H₁ H₂ : subgroup G then the commutator
⁅H₁, H₂⁆ : subgroup G
is the subgroup of
G generated by the commutators
h₁ * h₂ * h₁⁻¹ * h₂⁻¹.
Main definitions #
⁅g₁, g₂⁆ : the commutator of the elements
⁅H₁, H₂⁆ : the commutator of the subgroups
The commutator of two subgroups
The Three Subgroups Lemma (via the Hall-Witt identity)
The commutator of direct product is contained in the direct product of the commutators.
commutator_pi_pi_of_fintype for equality given
The commutator of a finite direct product is contained in the direct product of the commutators.