Correspondence_Theorem_Group_Theory
Provedcorrespondence-theoremproofwikiquotient-groups
Let G be a group and N a normal subgroup. Every subgroup of G/N is of the form H/N where N ≤ H ≤ G. The correspondence is a bijection.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Correspondence_Theorem_Group_Theory {G : Type _} [Group G] (N : Subgroup G) [hN : N.Normal] : ∀ H : Subgroup (G ⧸ N), ∃ K : Subgroup G, N ≤ K ∧ Subgroup.map (QuotientGroup.mk' N) K = H := by sorrySource