Null_Ring_iff_Zero_and_Unity_Coincide
Provednull-ringproofwikirings
The null ring is the only ring in which the unity and zero coincide. Equivalently, in a nontrivial ring, 1 ≠ 0.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Null_Ring_iff_Zero_and_Unity_Coincide {R : Type _} [Ring R] [Nontrivial R] : (1 : R) ≠ 0 := by sorrySource