Ordered scalar product #
In this file we define
OrderedSMul R M: an ordered additive commutative monoid
Rif the scalar product respects the order relation on the monoid and on the ring. There is a correspondence between this structure and convex cones, which is proven in
Implementation notes #
- We choose to define
Prop-valued mixin, so that it can be used for actions, modules, and algebras (the axioms for an "ordered algebra" are exactly that the algebra is ordered as a module).
- To get ordered modules and ordered vector spaces, it suffices to replace the
ordered module, ordered scalar, ordered smul, ordered action, ordered vector space
Scalar multiplication by positive elements preserves the order.
c • a < c • bfor some positive
a < b.
The ordered scalar product property is when an ordered additive commutative monoid with a partial order has a scalar multiplication which is compatible with the order.
To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first
To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
the first axiom of