mathlib

5e4b2d4a - feat(group_theory/group_action/quotient): If `G=<S>`, then `G / Z(G)` embeds into `S → {[g₁, g₂]}` (#17151)

feat(group_theory/group_action/quotient): If `G=<S>`, then `G / Z(G)` embeds into `S → {[g₁, g₂]}` (#17151) In other words, if a finitely generated group has finitely many commutators, then the center has index at most #commutators^rank. This is building up to the theorem that the size of the commutator subgroup is bounded in terms of the number of commutators.