Commit 2022-03-21 19:25 8001ea54
View on Github →feat(category_theory/abelian): right derived functor (#12841) This pr dualises derived.lean. Right derived functor and natural transformation between right derived functors and related lemmas are formalised. The docs string currently contains more than what is in this file, but everything else will come shortly after.