prime_of_isPrime — Mathlib

English

Conversely, if P is a prime ideal, then P is a prime element in the monoid of ideals.

Русский

И наоборот, если P — простой идеал, то он является простым элементом в моноиде идеалов.

LaTeX

$$$\text{IsPrime}(P) \Rightarrow \text{Prime}(P)$$$

Lean4

theorem prime_of_isPrime {P : Ideal A} (hP : P ≠ ⊥) (h : IsPrime P) : Prime P :=
  by
  refine ⟨hP, mt Ideal.isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩
  simpa only [Ideal.dvd_iff_le] using h.mul_le.mp (Ideal.le_of_dvd hIJ)

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