Ring_is_not_Empty
Provedproofwikirings
A ring cannot be empty.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Ring_is_not_Empty {R : Type _} [Ring R] : Nonempty R := by sorrySource
A ring cannot be empty.
import Mathlib.Algebra.Ring.Basic
theorem Ring_is_not_Empty {R : Type _} [Ring R] : Nonempty R := by sorry