instPosSMulMonoNatOfIsOrderedAddMonoid

English

For any ordered additive monoid M, the natural numbers act on M by a PosSMulMono structure: a number n ≥ 0 scales elements with order-preserving behavior.

Русский

Для упорядоченного аддитивного моноида M натуральные числа действуют по структуре PosSMulMono: n ≥ 0 масштабирует элементы и сохраняет порядок.

LaTeX

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

Lean4

instance {M : Type*} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] : PosSMulMono ℕ M where
  smul_le_smul_of_nonneg_left _n _ _a _b hab := nsmul_le_nsmul_right hab _

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