Theorems · Theorem · commutative algebra

Polynomial.height_eq_height_add_one

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (P : Ideal (Polynomial R)) [P.IsMaximal]
  [P.LiesOver p], P.height = p.height + 1

Let p be a prime ideal of R. If P is a maximal ideal of R[X] lying over p, ht(P) = ht(p) + 1.

Defined in

Mathlib.RingTheory.KrullDimension.Polynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingIdeal.IsMaximalIdeal.LiesOver