Theorem IsPGroup.mem_toSylow

Modification history

2024-11-04 01:46
Mathlib/GroupTheory/Sylow.lean
feat(GroupTheory/Sylow): A p-subgroup with index indivisible by p is a Sylow p-subgroup (#18573) …
Added IsPGroup.mem_toSylowView on Github →