mathlib

91ce9cbd - feat(group_theory/schreier): A theorem of Schur: A group with finitely many commutators has finite commutator subgroup (#17311)

feat(group_theory/schreier): A theorem of Schur: A group with finitely many commutators has finite commutator subgroup (#17311) This PR proves a theorem of Schur: a group with finitely many commutators has finite commutator subgroup. I also included an explicit bound that I will need later.