English
A commutative ring R is not a field if and only if there exists a prime ideal p ≠ ⊥.
Русский
Кольцо R не является полем тогда и только тогда существует простый идеал p, отличающийся от ⊥.
LaTeX
$$$\\neg\\mathrm{IsField}(R) \\iff \\exists p:\\mathrm{Ideal}(R),\\ p \\neq \\bot ∧ p.\\mathrm{IsPrime}$$$
Lean4
theorem not_isField_iff_exists_ideal_bot_lt_and_lt_top [Nontrivial R] : ¬IsField R ↔ ∃ I : Ideal R, ⊥ < I ∧ I < ⊤ :=
by
constructor
· intro h
obtain ⟨x, nz, nu⟩ := exists_not_isUnit_of_not_isField h
use Ideal.span { x }
rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top]
exact ⟨mt Ideal.span_singleton_eq_bot.mp nz, mt Ideal.span_singleton_eq_top.mp nu⟩
· rintro ⟨I, bot_lt, lt_top⟩ hf
obtain ⟨x, mem, ne_zero⟩ := SetLike.exists_of_lt bot_lt
rw [Submodule.mem_bot] at ne_zero
obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero
rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, ← hy] at lt_top
exact lt_top (I.mul_mem_right _ mem)
