Idempotent_Elements_of_Ring_with_No_Proper_Zero_Divisors
Provedidempotentsproofwikiringszero-divisors
Let (R, +, *) be a non-null ring with no proper zero divisors. Let x ∈ R. Then x * x = x iff x ∈ {0, 1}.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Idempotent_Elements_of_Ring_with_No_Proper_Zero_Divisors {R : Type _} [Ring R] [NoZeroDivisors R] (x : R) (h : x * x = x) : x = 0 ∨ x = 1 := by sorrySource