mathlib

9fe0cbc8 - feat(category_theory/preadditive/additive_functor): map_zero' is a redundant field, remove it (#10229)

feat(category_theory/preadditive/additive_functor): map_zero' is a redundant field, remove it (#10229) The map_zero' field in the definition of an additive functor can be deduced from the map_add' field. So we remove it.