English
Let R be a Commutative Semiring with a Linear Order and IsStrictOrderedRing. Then the positive subset { x ∈ R | 0 < x } is an IsOrderedMonoid under multiplication, i.e., left multiplication preserves order: a ≤ b implies a·c ≤ b·c for c ≥ 0.
Русский
Пусть R — коммутативная полусемирия с линейным порядком и IsStrictOrderedRing. Тогда положительная часть образует IsOrderedMonoid под умножением: если a ≤ b, то a·c ≤ b·c для c ≥ 0.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x : R \\\\mid 0 < x \\\\}, a \\\\le b \\\\Rightarrow a \\\\cdot c \\\\le b \\\\cdot c.$$$
Lean4
instance isOrderedMonoid [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
IsOrderedMonoid { x : R // 0 < x } :=
{ mul_le_mul_left := fun _ _ hxy c => Subtype.coe_le_coe.1 <| mul_le_mul_of_nonneg_left hxy c.2.le }
