mathlib

ed633868 - feat(category_theory/preadditive/injective) : definition of injective objects in a category (#11921)