toPosSMulReflectLE — Mathlib

English

If α is an ordered ring, then α together with itself forms an ordered module: IsOrderedModule α α.

Русский

Если α — упорядоченная кольцо, тогда α вместе с собой образуют упорядоченный модуль: IsOrderedModule α α.

LaTeX

$$$IsOrderedRing\;\alpha \Rightarrow IsOrderedModule\;\alpha\;\alpha$$$

Lean4

instance (priority := 100) toPosSMulReflectLE [PosSMulStrictMono α β] : PosSMulReflectLE α β where
  le_of_smul_le_smul_left _a ha _b₁ _b₂ := (strictMono_smul_left_of_pos ha).le_iff_le.1

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