Theorem Subgroup.card_commutator_le_of_finite_commutatorSet

Modification history

2023-06-06 04:38
Mathlib/GroupTheory/Schreier.lean
feat: port GroupTheory.Schreier (#4706)
Added Subgroup.card_commutator_le_of_finite_commutatorSetView on Github →