# Zulip Chat Archive

## Stream: maths

### Topic: ordered commutative monoid

#### Patrick Massot (Apr 05 2019 at 17:30):

/-- 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 (Apr 06 2019 at 14:10):

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 (Apr 06 2019 at 14:11):

Yeah, this comment is actually false

#### Chris Hughes (Apr 06 2019 at 14:40):

That comment should be about `ordered_cancel_comm_monoid`

, where `a + b ≤ a + c → b ≤ c`

implies cancellation

#### Patrick Massot (Apr 06 2019 at 14:56):

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`

Last updated: May 09 2021 at 09:11 UTC