Subset_Product_of_Normal_Subgroups_is_Normal
Provedgroup-theorynormal-subgroupproofwikisubset-product
If N and N' are normal subgroups of G, then their join (subset product) N ∨ N' is also a normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Subset_Product_of_Normal_Subgroups_is_Normal {G : Type _} [Group G] (N N' : Subgroup G) [hN : N.Normal] [hN' : N'.Normal] : (N ⊔ N').Normal := by sorrySource