Commit 2022-11-04 14:10 0f4c9091

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).