Left_Inverse_for_All_is_Right_Inverse
Provedinverse-elementsproofwikisemigroups
In a semigroup with a left identity where every element has a left inverse, the left inverse is also a right inverse.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Left_Inverse_for_All_is_Right_Inverse {S : Type _} [Semigroup S] (eL : S) (hL : ∀ a : S, eL * a = a) (hLinv : ∀ x : S, ∃ xL : S, xL * x = eL) (x xL : S) (hxL : xL * x = eL) : x * xL = eL := by sorrySource