Third_Isomorphism_Theorem
Provedgroup-theoryisomorphism-theoremproofwiki
The third isomorphism theorem: If N ≤ M are both normal in G, then (G/N)/(M/N) ≅ G/M.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Third_Isomorphism_Theorem {G : Type _} [Group G] (N M : Subgroup G) [hN : N.Normal] [hM : M.Normal] (hNM : N ≤ M) : Nonempty ((G ⧸ N) ⧸ (M.map (QuotientGroup.mk' N)) ≃* (G ⧸ M)) := by sorrySource