mathlib3

6aa0e30e - feat(category_theory/preadditive): additive functors preserve biproducts (#6882)

feat(category_theory/preadditive): additive functors preserve biproducts (#6882) An additive functor between preadditive categories creates and preserves biproducts. Also, renames `src/category_theory/abelian/additive_functor.lean` to `src/category_theory/preadditive/additive_functor.lean` as it so far doesn't actually rely on anything being abelian. Also, moves the `.map_X` lemmas about additive functors into the `functor` namespace, so we can use dot notation `F.map_add` etc, when `[functor.additive F]` is available. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>