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

@[deprecated Module.injective_of_isSemisimpleRing (since := "2025-09-12")]

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

Alias of Module.injective_of_isSemisimpleRing.

@[deprecated Module.projective_of_isSemisimpleRing (since := "2025-09-12")]

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

Alias of Module.projective_of_isSemisimpleRing.