# Commit 2022-11-04 14:10 0f4c9091

View on Github →feat(group_theory/abelianization): Add `commutator_representatives`

(#17312)
A theorem of Schur states that if `G`

has finitely many commutator elements `[g, h]`

, then the commutator subgroup of `G`

is finite. The first step of the proof is to reduce to the case where `G`

is finitely generated by passing to the subgroup generated by representatives `g`

and `h`

of the finitely many commutator elements in `G`

. This PR defines this subgroup (`closure_commutator_representatives`

) and provides the API needed for the proof of Schur's theorem (#17311).