Commutators of Subgroups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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_finite for equality given
The commutator of a finite direct product is contained in the direct product of the commutators.
The set of commutator elements
⁅g₁, g₂⁆ in