Internal_Group_Direct_Product_Isomorphism
Proveddirect-productgroup-theoryinternalisomorphismproofwiki
If H × K ≃ G via the multiplication map (an isomorphism), then both H and K are normal in G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Internal_Group_Direct_Product_Isomorphism {G : Type _} [Group G] (H K : Subgroup G) (h_inter : H ⊓ K = ⊥) (h_sup : H ⊔ K = ⊤) (h_comm : ∀ (h : H) (k : K), (h : G) * (k : G) = (k : G) * (h : G)) : H.Normal ∧ K.Normal := by sorrySource