Theorem Sylow.commutator_eq_bot_or_commutator_eq_self

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