Ordered algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring, for which scalar multiplication is "compatible" with the two orders.
The prototypical example is 2x2 matrices over the reals or complexes (or indeed any C^* algebra)
where the ordering the one determined by the positive cone of positive operators,
i.e. A ≤ B iff B - A = star R * R for some R.
(We don't yet have this example in mathlib.)
Implementation #
Because the axioms for an ordered algebra are exactly the same as those for the underlying
module being ordered, we don't actually introduce a new class, but just use the ordered_smul
mixin.
Tags #
ordered algebra
theorem
algebra_map_monotone
{R : Type u_1}
{A : Type u_2}
[ordered_comm_ring R]
[ordered_ring A]
[algebra R A]
[ordered_smul R A] :
monotone ⇑(algebra_map R A)