mathlib3

aa82ba00 - feat(algebra/opposites): add `add_opposite` (#11080)

feat(algebra/opposites): add `add_opposite` (#11080) Add `add_opposite`, add `to_additive` here and there. More `to_additive` can be added as needed later.