Commit 2024-12-28 18:52 1bf90b6e

View on Github →

feat(GroupTheory/SpecificGroups/ZGroup): A finite Z-group has cyclic commutator subgroup (#20183) One more step towards classifying finite Z-groups.

Estimated changes

Modified Mathlib/Algebra/Group/Hom/Basic.lean

added def MonoidHom.commGroupOfInjective

added def MonoidHom.commGroupOfSurjective

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

added theorem Subgroup.map_subgroupOf_eq_of_le

Modified Mathlib/GroupTheory/Abelianization.lean

added theorem Subgroup.map_subtype_commutator

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

added theorem IsZGroup.isCyclic_commutator