Projective Dimension in ModuleCat

theorem CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n

theorem CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) : projectiveDimension M = projectiveDimension N

theorem CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n

theorem CategoryTheory.projectiveDimension_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) : projectiveDimension M = projectiveDimension N