Def IsPGroup.toSylow

Modification history

2026-10-13 22:16

Mathlib/GroupTheory/Sylow.lean

chore(GroupTheory/Sylow): spell `Sylow` using `Maximal` (#44454) …

Modified IsPGroup.toSylow View on Github →

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 View on Github →