Identity_is_Unique
Provedalgebraic-structuresidentity-elementsidentity-is-uniqueproofwiki
Let be an algebraic structure that has an identity element . Then is unique.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Identity_is_Unique {M : Type*} [Mul M] (e₁ e₂ : M) (h₁ : ∀ a : M, e₁ * a = a ∧ a * e₁ = a) (h₂ : ∀ a : M, e₂ * a = a ∧ a * e₂ = a) : e₁ = e₂ := by sorrySource