Theorem Subgroup.relindex_dvd_card

Modification history

2024-12-20 19:39
Mathlib/GroupTheory/Index.lean
feat(GroupTheory/Transfer): A cyclic Sylow subgroup for the smallest prime has a normal complement (#19587) …
Added Subgroup.relindex_dvd_cardView on Github →