Def MonoidHom.commGroupOfInjective

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