Left_Inverse_and_Right_Inverse_is_Inverse
Provedinverse-elementsmonoidsproofwiki
In a monoid, if x has both a left inverse xL and right inverse xR, then xL = xR.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Left_Inverse_and_Right_Inverse_is_Inverse {M : Type _} [Monoid M] (x xL xR : M) (hL : xL * x = 1) (hR : x * xR = 1) : xL = xR := by sorrySource