instSMulPosStrictMonoIntOfIsOrderedAddMonoid

English

Alternate instance establishing PosSMulStrictMono for Int on ordered additive groups.

Русский

Альтернативный инстанс PosSMulStrictMono для целых на упорядоченных аддитивных группах.

LaTeX

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

Lean4

instance {G : Type*} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] : SMulPosStrictMono ℤ G where
  smul_lt_smul_of_pos_right _a ha _m _n hmn := zsmul_lt_zsmul_left ha hmn

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