mul_vecMulVec — Mathlib

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]

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