Theorems · Definition · commutative algebra
ringKrullDim
(R : Type u_1) → [CommSemiring R] → WithBot ℕ∞
The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.
- Defined in
- Mathlib.RingTheory.KrullDimension.Basic
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- ENatstatement · cited by 4,985
- WithBotstatement · cited by 1,498
- PrimeSpectrumproof · cited by 625
- Order.krullDimproof · cited by 82
Cited by77
Results whose statement or proof uses this declaration.
- ringKrullDim_eq_of_ringEquivstatement · cited by 9
- Ideal.height_le_ringKrullDim_of_ne_topstatement and proof · cited by 5
- ringKrullDim_eq_bot_of_subsingletonstatement · cited by 5
- Ring.krullDimLE_iffstatement · cited by 5
- IsLocalRing.maximalIdeal_height_eq_ringKrullDimstatement and proof · cited by 4
- ringKrullDim_le_of_surjectivestatement · cited by 4
- isRegularLocalRing_iffstatement and proof · cited by 4
- IsLocalization.AtPrime.ringKrullDim_eq_heightstatement · cited by 4
- Module.supportDim_quotient_eq_ringKrullDimstatement and proof · cited by 3
- Module.supportDim_self_eq_ringKrullDimstatement and proof · cited by 3
- ringKrullDim_quotient_succ_le_of_nonZeroDivisorstatement and proof · cited by 3
- Module.supportDim_eq_ringKrullDim_quotient_annihilatorstatement and proof · cited by 2