not_isField_iff_exists_prime — Mathlib

English

A commutative ring R is not a field if and only if there exists a prime ideal p with p ≠ ⊥.

Русский

Кольцо R не является полем тогда и только тогда существует простый идеал p, отличающийся от ⊥.

LaTeX

$$$\\neg\\mathrm{IsField}(R) \\iff \\exists p:\\mathrm{Ideal}(R),\\ p \\neq \\bot ∧ p.IsPrime$$$

Lean4

theorem not_isField_iff_exists_prime [Nontrivial R] : ¬IsField R ↔ ∃ p : Ideal R, p ≠ ⊥ ∧ p.IsPrime :=
  not_isField_iff_exists_ideal_bot_lt_and_lt_top.trans
    ⟨fun ⟨I, bot_lt, lt_top⟩ =>
      let ⟨p, hp, le_p⟩ := I.exists_le_maximal (lt_top_iff_ne_top.mp lt_top)
      ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.isPrime⟩,
      fun ⟨p, ne_bot, Prime⟩ => ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr Prime.1⟩⟩

Похожие утверждения