Ordered monoids #
This file provides the definitions of ordered monoids.
An ordered (additive) commutative monoid is a commutative monoid with a partial order such that addition is monotone.
Instances
An ordered commutative monoid is a commutative monoid with a partial order such that multiplication is monotone.
Instances
An ordered cancellative additive commutative monoid is a partially ordered commutative additive monoid in which addition is cancellative and monotone.
Instances
An ordered cancellative commutative monoid is a partially ordered commutative monoid in which multiplication is cancellative and monotone.
Instances
A linearly ordered additive commutative monoid.
Instances
A linearly ordered commutative monoid.
Instances
A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.
Instances
A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.