mathlib3

53f6d687 - feat(category_theory/preadditive) : definition of injective resolution (#12641)

feat(category_theory/preadditive) : definition of injective resolution (#12641) This pr is splitted from #12545. This pr contains the definition of: - `InjectiveResolution`; - `has_injective_resolution` and `has_injective_resolutions`; - injective object has injective resolution.