Unity_of_Ring_is_Unique
Provedproofwikiringsunity
A ring can have no more than one unity.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Unity_of_Ring_is_Unique {R : Type _} [Ring R] (e₁ e₂ : R) (h₁ : ∀ x, e₁ * x = x ∧ x * e₁ = x) (h₂ : ∀ x, e₂ * x = x ∧ x * e₂ = x) : e₁ = e₂ := by sorrySource