instSMulPosMonoNatOfIsOrderedAddMonoid

English

There is a natural-number version of PosSMulStrictMono: multiplication by a positive natural is strictly monotone.

Русский

Существуют натуральные показатели для PosSMulStrictMono: умножение положительного натурального на элемент строго монотонно.

LaTeX

$$$\\text{PosSMulStrictMono} \\; \\mathbb{N} \\; M$$$

Lean4

instance {M : Type*} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] : SMulPosMono ℕ M where
  smul_le_smul_of_nonneg_right _a ha _m _n hmn := nsmul_le_nsmul_left ha hmn

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