instIsOrderedModule — Mathlib

English

If M is an ordered module over R, then it is an ordered module over R≥0.

Русский

Если M является упорядоченным модулем над R, то он является упорядоченным модулем над R≥0.

LaTeX

$$$ IsOrderedModule \\ R\\ge 0\\ M $$$

Lean4

instance instIsOrderedModule [hM : IsOrderedModule R M] : IsOrderedModule R≥0 M
    where
  smul_le_smul_of_nonneg_left _b hb _a₁ _a₂ ha := hM.smul_le_smul_of_nonneg_left hb ha
  smul_le_smul_of_nonneg_right _b hb _a₁ _a₂ ha := hM.smul_le_smul_of_nonneg_right hb ha

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