mathlib3
a9781152 - refactor(category_theory/abelian): trivial generalisations (#12897)

Commit
3 years ago
refactor(category_theory/abelian): trivial generalisations (#12897) Trivial generalisations of some facts in `category_theory/abelian/non_preadditive.lean`. They are true more generally, and this refactor will make it easier to do some other clean-up I'd like to perform on abelian categories. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading