Zulip Chat Archive

Stream: maths

Topic: addition in opposite


view this post on Zulip Yury G. Kudryashov (Feb 26 2020 at 17:20):

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.

view this post on Zulip Yury G. Kudryashov (Feb 26 2020 at 17:20):

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

view this post on Zulip Reid Barton (Feb 26 2020 at 17:53):

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.

view this post on Zulip Reid Barton (Feb 26 2020 at 17:54):

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

view this post on Zulip Yury G. Kudryashov (Feb 26 2020 at 18:03):

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


Last updated: May 10 2021 at 07:15 UTC