Null_Ring_iff_Characteristic_is_One
Provedcharacteristicnull-ringproofwikiring-theory
The only ring whose characteristic is is the null ring.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Algebra.CharP.Basic
Formal statement
theorem Null_Ring_iff_Characteristic_is_One {R : Type _} [Ring R] : (∀ x : R, x = 0) ↔ CharP R 1 := by sorrySource