mathlib

0f4c9091 - feat(group_theory/abelianization): Add `commutator_representatives` (#17312)

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). Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>