# Category of abelian groups has enough injectives #

Given an abelian group `A`

, then `i : A ⟶ ∏_{A⋆} ℚ ⧸ ℤ`

defined by `i : a ↦ c ↦ c a`

is an
injective presentation for `A`

, hence category of abelian groups has enough injectives.

## Implementation notes #

This file is split from `Mathlib.Algebra.Grp.Injective`

is to prevent import loop.
This file's dependency imports `Mathlib.Algebra.Grp.Injective`

.