toSMulPosMonoNat — Mathlib

English

In a ordered semiring, the natural numbers act monotonically on α by multiplication.

Русский

В упорядоченном полугруппе натуральные числа действуют монотонно на α умножением.

LaTeX

$$$\text{SMulPosMono Nat α}$$$

Lean4

instance toSMulPosMonoNat [Semiring α] [PartialOrder α] [IsOrderedRing α] : SMulPosMono ℕ α where
  smul_le_smul_of_nonneg_right _a ha _m _n hmn := nsmul_le_nsmul_left ha hmn

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