Commit 2022-03-24 05:18 a9781152
View on Github →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.