instPosSMulStrictMonoIntOfIsOrderedAddMonoid

English

The same PosSMulStrictMono structure holds for Int acting on an ordered additive group G.

Русский

Та же структура PosSMulStrictMono действует для Int на упорядоченной аддитивной группе G.

LaTeX

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

Lean4

instance {G : Type*} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] : PosSMulStrictMono ℤ G where
  smul_lt_smul_of_pos_left _n hn _m₁ _m₂ := zsmul_lt_zsmul_right hn

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