Internal_Direct_Product_Theorem
Proveddirect-productgroup-theoryinternalproofwiki
If H and K are normal subgroups with H ∩ K = {e} and HK = G, then G is isomorphic to the direct product H × K.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Internal_Direct_Product_Theorem {G : Type _} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] (h_inter : H ⊓ K = ⊥) (h_sup : H ⊔ K = ⊤) : Nonempty (G ≃* H × K) := by sorrySource