isPrime_of_prime — Mathlib

English

If P is prime in the monoid of ideals, then P is a prime ideal in the ring sense.

Русский

Если P прост по монойде идеалов, то P является простым идеалом в смысле кольца.

LaTeX

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

Lean4

theorem isPrime_of_prime {P : Ideal A} (h : Prime P) : IsPrime P :=
  by
  refine ⟨?_, fun hxy => ?_⟩
  · rintro rfl
    rw [← Ideal.one_eq_top] at h
    exact h.not_unit isUnit_one
  · simp only [← Ideal.dvd_span_singleton, ← Ideal.span_singleton_mul_span_singleton] at hxy ⊢
    exact h.dvd_or_dvd hxy

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