vecMulVec_mulVec — Mathlib

English

Let u ∈ α^m and v,w ∈ α^m, then vecMulVec u v multiplies with w: vecMulVec u v *ᵥ w = (u · v) • w.

Русский

Пусть u ∈ α^m и v,w ∈ α^m. Тогда vecMulVec u v умножает на w так, что результат равен (u·v) • w.

LaTeX

$$$\operatorname{vecMulVec}(u,v) \; *ᵥ \; w = (u \cdot v) \; w$$$

Lean4

theorem vecMulVec_mulVec [Fintype n] (u : m → α) (v w : n → α) : vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u :=
  by
  ext i
  simp [mulVec, dotProduct, vecMulVec, Finset.mul_sum, mul_assoc]

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