Left_and_Right_Identity_are_the_Same
Provedidentity-elementsproofwiki
If an algebraic structure has a left identity eL and a right identity eR, then eL = eR.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Left_and_Right_Identity_are_the_Same {α : Type _} [Mul α] (eL eR : α) (hL : ∀ x : α, eL * x = x) (hR : ∀ x : α, x * eR = x) : eL = eR := by sorrySource