Group_Product_Identity_therefore_Inverses
Provedgroup-theoryproofwiki
In a group, if g * h = 1 then g = h⁻¹ and h = g⁻¹.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Group_Product_Identity_therefore_Inverses {G : Type _} [Group G] (g h : G) (hgh : g * h = 1) : g = h⁻¹ ∧ h = g⁻¹ := by sorrySource