Commit 2026-10-13 22:16 981a983f

View on Github →

chore(GroupTheory/Sylow): spell Sylow using Maximal (#44454) Replace Sylow.isPGroup' and Sylow.is_maximal' with a Maximal spelling: Maximal (IsPGroup p · : Subgroup G → Prop) toSubgroup

Estimated changes

Modified Mathlib/GroupTheory/Focal.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating/KleinFour.lean

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

Modified Mathlib/GroupTheory/Sylow.lean

modified def IsPGroup.toSylow

modified def Sylow.comapOfKerIsPGroup

added theorem Sylow.isPGroup

modified def Sylow.mapSurjective

Modified Mathlib/GroupTheory/Transfer.lean