∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M],
  CategoryTheory.projectiveDimension M =
    ⨆ p, CategoryTheory.projectiveDimension (M.localizedModule p.asIdeal.primeCompl)