Def MonoidHom.commGroupOfSurjective

Modification history

2024-12-28 18:52
Mathlib/Algebra/Group/Hom/Basic.lean
feat(GroupTheory/SpecificGroups/ZGroup): A finite Z-group has cyclic commutator subgroup (#20183) …
Added MonoidHom.commGroupOfSurjectiveView on Github →