2022-10-01 02:05
src/group_theory/schreier.lean
feat(group_theory/schreier): The size of the commutator subgroup is bounded in terms of the index of the center and the number of commutators (#16679) …
Added subgroup.card_commutator_dvd_index_center_pow