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 ≤ cimplies 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