Inverse_of_Subgroup
Provedproofwikisubgroupssubset-products
Let G be a group. Let H be a subgroup of G. Then H⁻¹ = H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Inverse_of_Subgroup {G : Type _} [Group G] (H : Subgroup G) (g : G) (hg : g ∈ H) : g⁻¹ ∈ H := by sorrySource