mathlib

9f5d911e - feat(category_theory/preadditive): inclusion functor from left exact functors to additive functors (#12339)