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 _ _ _