Identity_is_only_Idempotent_Cancellable_Element
Provedcancellabilityidempotenceidentity-elementsproofwiki
The identity is the only cancellable idempotent element in an algebraic structure with identity.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Identity_is_only_Idempotent_Cancellable_Element {M : Type _} [Monoid M] (x : M) (hidem : x * x = x) (hcancel : ∀ a b : M, x * a = x * b → a = b) : x = 1 := by sorrySource