toPosSMulMonoNat — Mathlib

English

In an ordered semiring, natural scalar multiplication is monotone: multiplication by a nonnegative natural preserves order.

Русский

В упорядоченном полугруппе по кольцу, умножение на неотрицательное натуральное число сохраняет порядок.

LaTeX

$$$\text{PosSMulMono Nat α}$$$

Lean4

instance toPosSMulMonoNat [Semiring α] [PartialOrder α] [IsOrderedRing α] : PosSMulMono ℕ α where
  smul_le_smul_of_nonneg_left _n _ _a _b hab := nsmul_le_nsmul_right hab _

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