Theorems · Theorem · commutative algebra

Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] {x : R},
  (∀ p ∈ (Module.annihilator R M).minimalPrimes, x ∉ p) →
    x ∈ (Module.annihilator R M).jacobson → Module.supportDim R (QuotSMulTop x M) + 1 = Module.supportDim R M

Defined in

Mathlib.RingTheory.KrullDimension.Regular

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingAddCommGroupModuleModule.Finite