mathlib3

362c2263 - refactor(category_theory): removing additive_category (#18903)

refactor(category_theory): removing additive_category (#18903) This PR removes the class `additive_category` which was essentially unused, and was creating instance issues during the port.