Injective objects in the category of $R$-modules

theorem Module.injective_object_of_injective_module (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [inj : Injective R M] : CategoryTheory.Injective ↧M

theorem Module.injective_module_of_injective_object (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [inj : CategoryTheory.Injective ↧M] : Injective R M

theorem Module.injective_iff_injective_object (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Injective R M ↔ CategoryTheory.Injective ↧M

instance ModuleCat.ulift_injective_of_injective (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Small.{v, u} R] [CategoryTheory.Injective ↧M] : CategoryTheory.Injective ↧(ULift.{v', v} M)