Commit 2022-03-04 17:34 ed633868
View on Github →feat(category_theory/preadditive/injective) : definition of injective objects in a category (#11921) This pr contains definition of injective objects and some useful instances.
feat(category_theory/preadditive/injective) : definition of injective objects in a category (#11921) This pr contains definition of injective objects and some useful instances.