mathlib3

f5138d15 - feat(category_theory/preadditive/*): algebra over endofunctor preadditive and forget additive functor (#15100)

feat(category_theory/preadditive/*): algebra over endofunctor preadditive and forget additive functor (#15100) This PR shows that the category of algebras over an endofunctor is preadditive and that forgetful functors from algebras over endofunctors and (co)algebras over (co)monads are additive.