HasExt instance for Module Category

If we assume Small.{v} R, the category ModuleCat.{v} R has enough projectives, which allows to introduce the instance HasExt.{v} (ModuleCat.{v} R). As a result, Ext-groups in this category of modules are defined and belong to Type v.

instance instHasExtModuleCatOfSmall (R : Type u) [Ring R] [Small.{v, u} R] : CategoryTheory.HasExt (ModuleCat R)