Commit 2025-01-13 10:02 143aee40

View on Github →

feat(GroupTheory/SpecificGroups/ZGroup): Commutator subgroup of a Z-group is a Hall subgroup (#20694) This PR proves that the commutator subgroup of a finite Z-group is a Hall subgroup. There are several intermediate results about p-groups and Sylow subgroups, but they require the heavy import of FieldTheory/Finite/Basic, so I decided to leave them in the Z-groups file.

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

added theorem IsPGroup.commutator_eq_bot_or_commutator_eq_self

added theorem IsPGroup.smul_mul_inv_trivial_or_surjective

added theorem IsZGroup.coprime_commutator_index

deleted theorem IsZGroup.isZGroup_of_coprime

added theorem Sylow.commutator_eq_bot_or_commutator_eq_self

added theorem Sylow.le_center_or_le_commutator

added theorem Sylow.normalizer_le_centralizer_or_le_commutator

added theorem Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator

added theorem isZGroup_of_coprime