toMulPosStrictMono — Mathlib

English

In a semiring with an ordered ring structure, the multiplication by a strictly positive element is strictly monotone on the right.

Русский

В полузаданном кольце с упорядоченной структурой умножение на строго положительный элемент на правой стороне является строго монотонным.

LaTeX

$$$ (a < b) \\Rightarrow (a c < b c) \\text{ for } c > 0. $$$

Lean4

instance (priority := 200) toMulPosStrictMono : MulPosStrictMono R where
  elim x _ _ h := IsStrictOrderedRing.mul_lt_mul_of_pos_right _ _ _ h x.prop

Похожие утверждения