If R
is a semisimple ring, then any R
-module is both injective and projective.
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
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