Product_of_Semigroup_Element_with_Right_Inverse_is_Idempotent
Provedidempotenceproofwikisemigroups
In a semigroup with a right identity, if xR is the right inverse of x, then xR * x is idempotent.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Product_of_Semigroup_Element_with_Right_Inverse_is_Idempotent {S : Type _} [Semigroup S] (eR : S) (x xR : S) (hR : ∀ a : S, a * eR = a) (hinv : x * xR = eR) : (xR * x) * (xR * x) = xR * x := by sorrySource