prime_iff_isPrime — Mathlib

English

For a nonzero ideal P, P is a prime element iff P is a prime ideal.

Русский

Для ненулевого идеала P он равен простому элементу тогда и только тогда, когда он является простым идеалом.

LaTeX

$$$\text{Prime}(P) \iff \text{IsPrime}(P)\quad\bigl(\text{for } P \neq 0\bigr)$$$

Lean4

/-- In a Dedekind domain, the (nonzero) prime elements of the monoid with zero `Ideal A`
are exactly the prime ideals. -/
theorem prime_iff_isPrime {P : Ideal A} (hP : P ≠ ⊥) : Prime P ↔ IsPrime P :=
  ⟨Ideal.isPrime_of_prime, Ideal.prime_of_isPrime hP⟩

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