ordered commutative monoid

Stream: maths

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/3525d212e3b3166b2f3cf1a5dc89114962630168/src/algebra/ordered_group.lean#L17-L20:

/-- An ordered (additive) commutative monoid is a commutative monoid
  with a partial order such that addition is an order embedding, i.e.
  `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=

Why?!? Why isn't it called ordered_add_comm_monoid, and where are the actual ordered_comm_monoid?

[Kevin Buzzard]

And another thing @Mario Carneiro -- are you sure the a + b ≤ a + c ↔ b ≤ c claim follows from the axioms you give to this structure? I'm thinking about with_bot int with addition defined by -infty + x = -infty.

[Patrick Massot]

Yeah, this comment is actually false

[Chris Hughes]

That comment should be about ordered_cancel_comm_monoid, where a + b ≤ a + c → b ≤ cimplies cancellation

[Patrick Massot]

This area of mathlib is really a mess anyway. If you feel like cleaning it up then you can take whatever you want from https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/linear_ordered_comm_group.lean In particular I did a to_multiplicative by hand (search and replace) in order to get back my lemmas for actual commutative monoid (ie. with multiplicative notation) but of course the correct way is to patch mathlib to use multiplication and decorate everything with to_additive