Theorems · Theorem · commutative algebra
ringKrullDim_le_ringKrullDim_quotSMulTop_succ
∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {x : R},
x ∈ IsLocalRing.maximalIdeal R → ringKrullDim R ≤ ringKrullDim (R ⧸ x • ⊤) + 1- Cited by
- 0 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Top.topstatement and proof · cited by 9,680
- ENatstatement and proof · cited by 4,985
- Idealstatement · cited by 4,748
- HasQuotient.Quotientstatement and proof · cited by 2,301
- WithBotstatement and proof · cited by 1,498
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealstatement and proof · cited by 297
- IsNoetherianRingstatement and proof · cited by 268
- Submodule.pointwiseDistribMulActionstatement · cited by 105
- ringKrullDimstatement and proof · cited by 75
- Module.supportDimproof · cited by 23
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.