## Stream: maths

#### 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.

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

(OK, PRs+issues)

#### Mario Carneiro (Jun 09 2020 at 06:34):

not all open I hope :shock:

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: May 14 2021 at 19:21 UTC