Theorems · Theorem · commutative algebra

Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {r : R},
  r ∈ nonZeroDivisors R →
    ∀ {p : Ideal R} [p.IsPrime],
      ↑p.height = ringKrullDim R → r ∈ p → ringKrullDim (R ⧸ Ideal.span {r}) + 1 = ringKrullDim R

If r is a nonzerodivisor contained in an ideal of maximal height, dim (R / (r)) + 1 = dim R.

Defined in

Mathlib.RingTheory.KrullDimension.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingIdeal.IsPrime