vecMul_vecMulVec — Mathlib

English

For Fintype m, and u,v,w with u,v : m→α and w : n→α, the contraction vecMulVec yields a scalar times a vector: uᵥ* vecMulVec v w = (u·v) • w.

Русский

Пусть m конечен; u,v : m → α и w : n → α. Тогда uᵥ* vecMulVec v w = (u·v) • w, т.е. норма ⟨u,v⟩ умножается на w.

LaTeX

$$$u^{\top} \operatorname{vecMulVec}(v,w) = (u \cdot v) \; w$$$

Lean4

theorem vecMul_vecMulVec [Fintype m] (u v : m → α) (w : n → α) : u ᵥ* vecMulVec v w = (u ⬝ᵥ v) • w :=
  by
  ext i
  simp [vecMul, dotProduct, vecMulVec, Finset.sum_mul, mul_assoc]

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