Zulip Chat Archive
Stream: maths
Topic: ordered add monoids
Yury G. Kudryashov (Jun 09 2020 at 05:37):
What is the hierarchy of ordered_*_monoid classes?
Yury G. Kudryashov (Jun 09 2020 at 05:37):
What is the most general class with a ≤ b → c ≤ d → a + c ≤ b + d?
Johan Commelin (Jun 09 2020 at 06:28):
Isn't that just ordered_add_monoid?
Yury G. Kudryashov (Jun 09 2020 at 06:30):
How is it related to ordered_cancel_add_comm_monoid?
Yury G. Kudryashov (Jun 09 2020 at 06:31):
It seems that the latter is stronger.
Johan Commelin (Jun 09 2020 at 06:31):
Yup
Johan Commelin (Jun 09 2020 at 06:31):
In that one, (+) a is strongly monotone
Yury G. Kudryashov (Jun 09 2020 at 06:34):
In the meantime we've reached 3K PRs
Yury G. Kudryashov (Jun 09 2020 at 06:34):
(OK, PRs+issues)
Mario Carneiro (Jun 09 2020 at 06:34):
not all open I hope :shock:
Yury G. Kudryashov (Jun 09 2020 at 06:34):
Sure
Yury G. Kudryashov (Jun 09 2020 at 06:35):
I meant that we have #3001
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: Dec 20 2023 at 11:08 UTC