Theorem Sylow.normalizer_le_centralizer_or_le_commutator

Modification history

2025-01-13 10:02
Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
feat(GroupTheory/SpecificGroups/ZGroup): Commutator subgroup of a Z-group is a Hall subgroup (#20694) …
Added Sylow.normalizer_le_centralizer_or_le_commutatorView on Github →