Internal_Group_Direct_Product_of_Normal_Subgroups
Proveddirect-productgroup-theorynormal-subgroupproofwiki
If H and K are normal subgroups of G with H ∩ K = {e}, then every element of H commutes with every element of K.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Internal_Group_Direct_Product_of_Normal_Subgroups {G : Type _} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] (h_inter : H ⊓ K = ⊥) : ∀ (h : H) (k : K), (h : G) * (k : G) = (k : G) * (h : G) := by sorrySource