Commit 2022-11-15 10:09 5e4b2d4a

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.