Theorems · Theorem · algebraic geometry

PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain

∀ {A : Type u} [inst : CommRing A] [IsDomain A] [IsNoetherianRing A],
  ¬IsField A →
    ∀ {I : Ideal A},
      I ≠ ⊥ → ∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥

In a Noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product or prime ideals ([samuel1967, § 3.3, Lemma 3])

Defined in

Mathlib.RingTheory.Spectrum.Prime.Basic

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainIsNoetherianRing