instOrderedSMul — Mathlib

English

If M carries an ordered scalar action by R, then the dual order on M also carries an OrderedSMul structure with the same action.

Русский

Если у M задано упорядоченное действие R на M, то на M^{op} также существует упорядоченное действие с тем же скаляром.

LaTeX

$$$ OrderedSMul\ R\ M^{op} . $$$

Lean4

instance instOrderedSMul : OrderedSMul R Mᵒᵈ
    where
  smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M)
  lt_of_smul_lt_smul_of_pos := OrderedSMul.lt_of_smul_lt_smul_of_pos (M := M)

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