mulVec_smul_assoc — Mathlib

English

For an integer x and vector v, the vecMul with x on the right equals the scalar multiplication by x cast to α on v, namely v ᵥ* x = (x : α) • v.

Русский

Для целого числа x и вектора v верно v ᵥ* x = (x : α) • v, т. е. vecMul по правой стороне равняется скалярному умножению на образ x в α.

LaTeX

$$$v ᵥ* x = (x : α) \\cdot v$$$

Lean4

@[deprecated mulVec_smul (since := "2025-08-14")]
theorem mulVec_smul_assoc [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) : A *ᵥ (a • b) = a • A *ᵥ b :=
  mulVec_smul _ _ _

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