Theorems · Theorem · commutative algebra

Module.supportDim_le_supportDim_quotSMulTop_succ_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},
  x ∈ (Module.annihilator R M).jacobson → Module.supportDim R M ≤ Module.supportDim R (QuotSMulTop x M) + 1

Defined in: Mathlib.RingTheory.KrullDimension.Regular
Cited by: 2 results in Mathlib
Foundations: Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsNoetherianRing AddCommGroup Module Module.Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites57

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Top.topstatement · cited by 9,680
Submodulestatement · cited by 7,192
Set.Elemproof · cited by 7,166
ENatstatement and proof · cited by 4,985
Idealstatement · cited by 4,748
Bot.botproof · cited by 4,720
LE.le.transproof · cited by 3,151
Nontrivialproof · cited by 2,416
le_reflproof · cited by 2,061

Cited by2

Results whose statement or proof uses this declaration.

Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobsonproof · cited by 2
Module.supportDim_le_supportDim_quotSMulTop_succproof · cited by 1