mathlib3

362844dc - feat(category_theory/preadditive): a category induced from a preadditive category is preadditive (#6883)