Group_is_Inverse_Semigroup_with_Identity
Provedgroup-theoryproofwiki
A group is an inverse semigroup with an identity: for every element a, a * a⁻¹ * a = a and a⁻¹ * a * a⁻¹ = a⁻¹.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Group_is_Inverse_Semigroup_with_Identity {G : Type _} [Group G] (a : G) : a * a⁻¹ * a = a ∧ a⁻¹ * a * a⁻¹ = a⁻¹ := by sorrySource