toOrderedSMul — Mathlib

English

In a LinearOrderedSemiring that is IsStrictOrderedRing, the canonical action of R on R (multiplication) is an OrderedSMul.

Русский

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

LaTeX

$$$ OrderedSMul R R. $$$

Lean4

instance toOrderedSMul : OrderedSMul R R :=
  OrderedSMul.mk'' fun _ => strictMono_mul_left_of_pos

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