Internal_Group_Direct_Product_is_Injective
Proveddirect-productgroup-theoryinternalproofwiki
If H ∩ K = {e}, then the multiplication map H × K → G is injective.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Internal_Group_Direct_Product_is_Injective {G : Type _} [Group G] (H K : Subgroup G) (h_inter : H ⊓ K = ⊥) : Function.Injective (fun p : H × K => (p.1 : G) * (p.2 : G)) := by sorrySource