mathlib documentation

algebra.category.Group.injective

Injective objects in the category of abelian groups #

In this file we prove that divisible groups are injective object in category of (additive) abelian groups.

@[protected, instance]