Documentation

Mathlib.RingTheory.SimpleModule.InjectiveProjective

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