Theorem Subgroup.map_subgroupOf_eq_of_le

Modification history

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