Inverses_in_Subgroup
Provedproofwikisubgroups
Let G be a group. Let H be a subgroup of G. Then for each h in H, the inverse of h in H is the same as the inverse of h in G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Inverses_in_Subgroup {G : Type _} [Group G] (H : Subgroup G) (h : G) (hH : h ∈ H) : h⁻¹ ∈ H := by sorrySource