val_nnqsmul — Mathlib

English

For q ∈ ℚ≥0 and x ∈ selfAdjoint(R), the underlying value of the scaled element equals the same rational multiple of the underlying value, i.e., ↑(q • x) = q • (x : R).

Русский

Для q ∈ ℚ≥0 и x ∈ selfAdjoint(R) приведённое значение масштабирующего элемента равно той же дроби: ↑(q • x) = q • (x : R).

LaTeX

$$$ \\uparrow (q \\cdot x) = q \\cdot (x) \\quad \\text{for } q \\in \\mathbb{Q}_{\\ge 0},\\; x \\in \\mathrm{selfAdjoint}(R). $$$

Lean4

@[simp, norm_cast]
theorem val_nnqsmul (q : ℚ≥0) (x : selfAdjoint R) : ↑(q • x) = q • (x : R) :=
  rfl

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