Theorems · Theorem · commutative algebra

Ideal.height_le_iff_exists_minimalPrimes

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (n : ℕ∞),
  p.height ≤ n ↔ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

In a commutative Noetherian ring R, a prime ideal p has height no greater than n if and only if it is a minimal ideal over some ideal generated by no more than n elements.

Defined in

Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingIdeal.IsPrime