addition in opposite

Stream: maths

[Yury G. Kudryashov]

Currently op (a * b) = op b * op a while op (a + b) = op a + op b. Though it makes sense because addition is usually commutative, it breaks the to_additive machinery.

[Yury G. Kudryashov]

What was the reason to choose op (a + b) = op a + op b?

[Reid Barton]

In general it doesn't make sense to conflate different kinds of "opposite" because they can vary independently: eg multiplication and order (or symmetric monoidal structure and category structure). I think this was discussed on either zulip or the github pr.

[Reid Barton]

For additive purposes maybe it makes sense to add opposite_add (which strikes me as rarely useful otherwise)

[Yury G. Kudryashov]

I'll either add opposite_add or use additive/multiplicative tags instead of to_additive.