vecMul_eq_sum — Mathlib

English

A row-vector is obtained as a linear combination of the rows of a matrix with coefficients given by a vector.

Русский

Вектор-строка задаётся как линейная комбинация строк матрицы с коэффициентами, заданными вектором.

LaTeX

$$$v^{\top} M = \sum_i v_i \; M_i,$ where $M_i$ denotes the i-th row of $M$.$$

Lean4

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

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