Category of $R$-modules has enough injectives

we lift enough injectives of abelian groups to arbitrary $R$-modules by adjoint functors restrictScalars ⊣ coextendScalars

instance instEnoughInjectivesModuleCatInt : CategoryTheory.EnoughInjectives (ModuleCat ℤ)

theorem ModuleCat.enoughInjectives (R : Type u) [Ring R] : CategoryTheory.EnoughInjectives (ModuleCat R)

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