Theorem IsZGroup.coprime_commutator_index

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