Ideals_of_Field
Provedfieldsidealsproofwiki
A commutative ring with unity R is a field iff the only ideals of R are R itself and {0}.
Preamble
import Mathlib.RingTheory.Ideal.Basic import Mathlib.Algebra.Field.Basic
Formal statement
theorem Ideals_of_Field {R : Type _} [CommRing R] [Nontrivial R] : (∀ I : Ideal R, I = ⊤ ∨ I = ⊥) ↔ IsField R := by sorrySource