English
For Fintype m, matrices M ∈ M(l,m;α), and vectors x ∈ α^m, y ∈ α^n, we have M · vecMulVec x y = vecMulVec (M·x) y, i.e., left multiplication distributes through vecMulVec.
Русский
Пусть M ∈ M(l,m), и векторы x ∈ α^m, y ∈ α^n. Тогда M · vecMulVec(x,y) = vecMulVec(M·x, y).
LaTeX
$$$M \; vecMulVec(x,y) = vecMulVec(M \!\cdot x, y)$$$
Lean4
theorem mul_vecMulVec [Fintype m] (M : Matrix l m α) (x : m → α) (y : n → α) :
M * vecMulVec x y = vecMulVec (M *ᵥ x) y := by
ext
simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]