Structures · Algebra

CanonicallyOrderedAdd

An ordered additive monoid is CanonicallyOrderedAdd if the ordering coincides with the subtractibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial ordered groups. We have a ≤ b + a and a ≤ a + b as separate fields. In the commutative case the second field is redundant, but in the noncommutative case (satisfied most relevantly by the ordinals), this extra field allows us to prove more things without the extra commutativity assumption.

Defined in

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Shape

One type argument · adds le_add_self, le_self_add