qsmul_of_nonpos — Mathlib

English

If a ≤ 0 then a • x equals the negative of the nonnegative rational action on x.

Русский

Если $a \\le 0$, то $a\\cdot x$ равняется минусу неотрицательного рационального действия на $x$.

LaTeX

$$$a\\le 0 \\Rightarrow a\\cdot x = -((|a|)\\cdot x)$$$

Lean4

theorem qsmul_of_nonpos {a : ℚ} (h : a ≤ 0) (x : DivisibleHull M) :
    a • x = -((show ℚ≥0 from ⟨-a, Left.nonneg_neg_iff.mpr h⟩) • x) :=
  by
  have := h.eq_or_lt
  aesop (add simp [qsmul_def, abs_of_neg])

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