isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors

English

If α is a principal ideal ring with no zero divisors and nontrivial, then for any P, P is prime iff P = ⊥ or P = span{p} for some prime p.

Русский

Если α — кольцо с главными идеалами без нулевых делителей и ненулевое, то для любого P: Pprime тогда, когда P = ⊥ или P = span{p} для некоторого простого p.

LaTeX

$$$P.IsPrime \\iff P = \\perp \\lor \\exists p, Prime p \\land P = \\operatorname{span}\\{p\\}.$$$

Lean4

theorem isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors [NoZeroDivisors α] [Nontrivial α] {P : Ideal α} :
    P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = span { p } :=
  by
  rw [or_iff_not_imp_left, ← forall_congr' isPrime_iff_of_isPrincipalIdealRing, ← or_iff_not_imp_left,
    or_iff_right_of_imp]
  rintro rfl; exact bot_prime

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