dotProduct_mulVec — Mathlib

English

For vectors v ∈ R^m, w ∈ R^n, and a matrix A ∈ M_{m×n}(R), dot(v, A w) = dot(A^T v, w).

Русский

Для векторов v ∈ R^m, w ∈ R^n и матрицы A ∈ M_{m×n}(R) выполняется скалярное произведение: ⟨v, A w⟩ = ⟨A^T v, w⟩.

LaTeX

$$$\langle v, A w \rangle = \langle A^T v, w \rangle$$$

Lean4

/-- Associate the dot product of `mulVec` to the left. -/
theorem dotProduct_mulVec [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) :
    v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w :=
  by
  simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
  exact Finset.sum_comm

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