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