ordered_comm_monoid_with_zero

Stream: Is there code for X?

[Yaël Dillies]

It seems that we're missing the infimum of docs#linear_ordered_comm_monoid_with_zero and docs#ordered_semiring. Do they not come up in maths?

[Yaël Dillies]

For the record, that means docs#order_monoid_with_zero has an unneeded linearity assumption for now.

[Reid Barton]

Can you give a math definition?

[Yaël Dillies]

linear_ordered_comm_monoid_with_zero - linearity

[Reid Barton]

I mean I'm not really sure that linear_ordered_comm_monoid_with_zero "comes up" in math in the first place, other than in the sense that there are lots of examples of them.