orderedSMul — Mathlib

English

If M is an AddCommGroup with LinearOrder and IsOrderedAddMonoid, then the integers act on M with an order-preserving action.

Русский

Пусть M — добавочно-коммутативная группа с линейным порядком; целые числа действуют на M естественным образом, сохраняя порядок.

LaTeX

$$$ OrderedSMul\ Z\ M. $$$

Lean4

instance orderedSMul [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : OrderedSMul ℤ M :=
  OrderedSMul.mk'' fun n hn => by
    cases n
    · simp only [Int.ofNat_eq_coe, Int.natCast_pos, natCast_zsmul] at hn ⊢
      exact strictMono_smul_left_of_pos hn
    · cases (Int.negSucc_not_pos _).1 hn

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