Modules over a division ring are injective

Every module over a division ring is injective. By Baer's criterion it suffices to extend maps from left ideals, and a left ideal of a division ring is zero or the whole ring.

instance Module.Injective.of_divisionRing (D : Type u) [DivisionRing D] (M : Type v) [AddCommGroup M] [Module D M] : Injective D M

Every module over a division ring is injective.