toSMulPosStrictMonoNat — Mathlib

English

In a strict ordered semiring, the natural scalars act with PosSMulStrictMono.

Русский

В строгом упорядоченном кольце натуральные скаляры действуют с PosSMulStrictMono.

LaTeX

$$$\text{PosSMulStrictMono Nat α}$$$

Lean4

instance toSMulPosStrictMonoNat [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] : SMulPosStrictMono ℕ α where
  smul_lt_smul_of_pos_right _a ha _m _n hmn := nsmul_lt_nsmul_left ha hmn

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