mulVec_eq_sum — Mathlib

English

The vector product M *ᵥ v equals the finite sum over i of (v_i) times the i-th row of M transposed.

Русский

Векторное произведение M *ᵥ v равно конечной сумме по i от (v_i) умноженного на i-ю строку M в транспонированном виде.

LaTeX

$$$M *^{} v = \\sum_{i} (v_i) \\cdot M^{\\top}_{i}.$$$

Lean4

theorem mulVec_eq_sum [Fintype n] (v : n → α) (M : Matrix m n α) : M *ᵥ v = ∑ i, MulOpposite.op (v i) • Mᵀ i :=
  (Finset.sum_fn ..).symm

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