mathlib

cd942870 - feat(category_theory/abelian): right derived functor in abelian category with enough injectives (#12810)

feat(category_theory/abelian): right derived functor in abelian category with enough injectives (#12810) This pr shows that in an abelian category with enough injectives, if a functor preserves finite limits, then the zeroth right derived functor is naturally isomorphic to itself. Dual to #12403 ↔️ Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: mcdoll <moritz.doll@googlemail.com> Co-authored-by: Jakob von Raumer <jakob@von-raumer.de> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>