Commit 2022-03-18 18:32 d17ecf9e

feat(category_theory/abelian) : injective resolutions of an object in a category with enough injectives (#12545) This pr dualises src/category_theory/preadditive/projective_resolution.lean. But since half of the file requires abelian assumption, I moved it to src/category_theory/abelian/*. The reason it needs abelian assumption is because I want class inference to deduce exact f g from exact g.op f.op.