isPrime_iff_bot_or_prime — Mathlib

English

In a Dedekind domain, every nonzero ideal is either the zero element or a prime element.

Русский

В детерминантном домене каждый ненулевой идеал либо нулевой элемент, либо простой элемент.

LaTeX

$$$\text{IsPrime}(P) \iff P = \bot \lor \text{Prime}(P)$$$

Lean4

/-- In a Dedekind domain, the prime ideals are the zero ideal together with the prime elements
of the monoid with zero `Ideal A`. -/
theorem isPrime_iff_bot_or_prime {P : Ideal A} : IsPrime P ↔ P = ⊥ ∨ Prime P :=
  ⟨fun hp => (eq_or_ne P ⊥).imp_right fun hp0 => Ideal.prime_of_isPrime hp0 hp, fun hp =>
    hp.elim (fun h => h.symm ▸ Ideal.bot_prime) Ideal.isPrime_of_prime⟩

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