Commit 2024-12-23 10:59 f12cb0ca

View on Github →

feat(GroupTheory/SpecificGroups/ZGroup): Extension of coprime Z-groups is a Z-group (#20147) One more step towards showing that every finite Z-group is a semidirect product of cyclic groups of coprime order.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Ker.lean

added theorem Subgroup.ker_subgroupMap

Modified Mathlib/GroupTheory/Index.lean

modified theorem Subgroup.relindex_dvd_card

Modified Mathlib/GroupTheory/PGroup.lean

added theorem IsPGroup.le_or_disjoint_of_coprime

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

added theorem IsPGroup.isCyclic_of_isZGroup

added theorem IsZGroup.isZGroup_of_coprime

Modified Mathlib/GroupTheory/Transfer.lean