qsmul_def — Mathlib

English

The action of a rational a on an element x of DivisibleHull M is given by a standard explicit formula in terms of the sign of a and the absolute value |a|.

Русский

Действие рационального числа $a$ на элемент $x$ в DivisibleHull M задаётся по явной формуле через знак $a$ и модуль $|a|$.

LaTeX

$$$a\\cdot x = (\\operatorname{sign} a)_{\\mathbb{Z}} \\cdot (|a|)_{\\mathbb{Q}_{\\ge 0}} \\cdot x$$$

Lean4

theorem qsmul_def (a : ℚ) (x : DivisibleHull M) :
    a • x = (SignType.sign a : ℤ) • (show ℚ≥0 from ⟨|a|, abs_nonneg _⟩) • x :=
  rfl

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