Theorem IsPGroup.toSylow_coe

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.toSylow_coeView on Github →