Theorem Subgroup.comap_eq_ker_of_surjective

Modification history

2026-06-24 00:45
Mathlib/Algebra/Group/Subgroup/Ker.lean
feat(GroupTheory/IsPerfect): Grün's lemma (#39956) …
Added Subgroup.comap_eq_ker_of_surjectiveView on Github →