instPosSMulStrictMonoNatOfIsOrderedAddMonoid

English

There is an integer version of PosSMulStrictMono: multiplying by a positive integer reflects strict order.

Русский

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

LaTeX

$$$\\text{PosSMulStrictMono} \\\\; \\mathbb{Z} \\\\; G$$$

Lean4

instance {M : Type*} [PartialOrder M] [AddCancelCommMonoid M] [IsOrderedAddMonoid M] : PosSMulStrictMono ℕ M where
  smul_lt_smul_of_pos_left _n hn _m₁ _m₂ := nsmul_lt_nsmul_right hn.ne'

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