instIsStrictOrderedModule — Mathlib

English

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

Русский

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

LaTeX

$$$ IsStrictOrderedModule \\ R\\ge 0\\ M $$$

Lean4

instance instIsStrictOrderedModule [hM : IsStrictOrderedModule R M] : IsStrictOrderedModule R≥0 M
    where
  smul_lt_smul_of_pos_left _b hb _a₁ _a₂ ha := hM.smul_lt_smul_of_pos_left hb ha
  smul_lt_smul_of_pos_right _b hb _a₁ _a₂ ha := hM.smul_lt_smul_of_pos_right hb ha

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