Preimage_of_Normal_Subgroup_of_Quotient_Group_under_Quotient_Epimorphism_is_Normal
Provednormal-subgroupsproofwikiquotient-groups
Let H be a normal subgroup of G, K a normal subgroup of G/H. Then the preimage of K under the quotient map is normal in G.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Preimage_of_Normal_Subgroup_of_Quotient_Group_under_Quotient_Epimorphism_is_Normal {G : Type _} [Group G] (N : Subgroup G) [hN : N.Normal] (K : Subgroup (G ⧸ N)) [hK : K.Normal] : (K.comap (QuotientGroup.mk' N)).Normal := by sorrySource