Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes