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