Subset_Product_of_Subgroups
Provedproofwikisubgroupssubset-product-of-subgroupssubset-products
Let G be a group. Let H, K be subgroups. Then H * K is a subgroup iff H and K are permutable.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subset_Product_of_Subgroups {G : Type _} [Group G] (H K : Subgroup G) (a : G) (ha : a ∈ H) (b : G) (hb : b ∈ K) : a * b ∈ (H ⊔ K : Subgroup G) := by sorrySource