Global Dimension of Regular Local Ring is equal to Krull Dimension

theorem finite_projectiveDimension_of_isRegularLocalRing_aux {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] (i : ℕ) : ↑(IsLocalRing.depth M) + ↑i ≥ ringKrullDim R → ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE M n

theorem projectiveDimension_ne_top_of_isRegularLocalRing {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.projectiveDimension M ≠ ⊤

theorem IsRegularLocalRing.globalDimension_eq_ringKrullDim (R : Type u) [CommRing R] [Small.{v, u} R] [IsRegularLocalRing R] : globalDimension R = ringKrullDim R

theorem IsRegularRing.globalDimension_eq_ringKrullDim (R : Type u) [CommRing R] [Small.{v, u} R] [IsRegularRing R] : globalDimension R = ringKrullDim R