Ordered groups #
This file defines bundled ordered groups and develops a few basic results.
Implementation details #
Unfortunately, the number of '
appended to lemmas in this file
may differ between the multiplicative and the additive version of a lemma.
The reason is that we did not want to change existing names in the library.
An ordered additive commutative group is an additive commutative group with a partial order in which addition is strictly monotone.
An ordered commutative group is a commutative group with a partial order in which multiplication is strictly monotone.
Alias of mul_lt_mul_left'
.
Alias of le_of_mul_le_mul_left'
.
Alias of lt_of_mul_lt_mul_left'
.
Linearly ordered commutative groups #
A linearly ordered additive commutative group is an additive commutative group with a linear order in which addition is monotone.
A linearly ordered commutative group is a commutative group with a linear order in which multiplication is monotone.