Product_of_Subgroup_with_Itself
Provedproofwikisubgroupssubset-products
Let G be a group. Then for all subgroups H of G, H * H = H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Product_of_Subgroup_with_Itself {G : Type _} [Group G] (H : Subgroup G) (g : G) (hg : g ∈ H) : ∃ a b : G, a ∈ H ∧ b ∈ H ∧ a * b = g := by sorrySource