Subset_Product_with_Normal_Subgroup_as_Generator_v4
Provedgroup-theorynormal-subgroupproofwikisubset-product
If H is a subgroup and N is a normal subgroup of G, then for any n in N and h in H, n*h is in N ∨ H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Subset_Product_with_Normal_Subgroup_as_Generator_v4 {G : Type _} [Group G] (H : Subgroup G) (N : Subgroup G) [hN : N.Normal] : ∀ (n : G) (h : G), n ∈ N → h ∈ H → n * h ∈ N ⊔ H := by sorrySource