Inverse_of_Identity_Element_is_Itself
Provedidentity-elementsinverse-elementsproofwiki
The inverse of the identity element is itself.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Inverse_of_Identity_Element_is_Itself {G : Type _} [Group G] : (1 : G)⁻¹ = 1 := by sorrySource