minimalPrimes_eq_empty_iff — Mathlib

English

The set of minimal primes of I is empty if and only if I equals the top ideal.

Русский

Набор минимальных primes над I пуст тогда и только тогда I = ⊤.

LaTeX

$$$I.minimalPrimes = \emptyset \iff I = \top$$$

Lean4

theorem minimalPrimes_eq_empty_iff (I : Ideal R) : I.minimalPrimes = ∅ ↔ I = ⊤ :=
  by
  constructor
  · intro e
    by_contra h
    have ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
    have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'
    rw [e] at hp
    apply Set.notMem_empty _ hp.1
  · rintro rfl
    exact Ideal.minimalPrimes_top

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