Theorem Subgroup.rank_commutator_le_card

Modification history

2025-07-23 15:29
Mathlib/GroupTheory/Commutator/Finite.lean
chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) …
Added Subgroup.rank_commutator_le_cardView on Github →