Zulip Chat Archive

Stream: maths

Topic: ordered add monoids


view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 05:37):

What is the hierarchy of ordered_*_monoid classes?

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 05:37):

What is the most general class with a ≤ b → c ≤ d → a + c ≤ b + d?

view this post on Zulip Johan Commelin (Jun 09 2020 at 06:28):

Isn't that just ordered_add_monoid?

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:30):

How is it related to ordered_cancel_add_comm_monoid?

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:31):

It seems that the latter is stronger.

view this post on Zulip Johan Commelin (Jun 09 2020 at 06:31):

Yup

view this post on Zulip Johan Commelin (Jun 09 2020 at 06:31):

In that one, (+) a is strongly monotone

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:34):

In the meantime we've reached 3K PRs

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:34):

(OK, PRs+issues)

view this post on Zulip Mario Carneiro (Jun 09 2020 at 06:34):

not all open I hope :shock:

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:34):

Sure

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 06:35):

I meant that we have #3001

view this post on Zulip Mario Carneiro (Jun 09 2020 at 06:36):

Oh I see. If we are going for 3K there are still 71 to go though


Last updated: May 14 2021 at 19:21 UTC