If R is a semisimple ring, then any R-module is both injective and projective.

theorem Module.injective_of_isSemisimpleRing (R : Type u_1) [Ring R] [IsSemisimpleRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : Injective R M

theorem Module.projective_of_isSemisimpleRing (R : Type u_1) [Ring R] [IsSemisimpleRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : Projective R M