mulVec_diagonal — Mathlib

English

The product of a diagonal matrix diag(v) with a vector w has i-th entry equal to v(i)·w(i).

Русский

Произведение диагональной матрицы diag(v) на вектор w имеет i-ю компоненту, равную v(i)·w(i).

LaTeX

$$$(\mathrm{diag}(v) \cdot w)_i = v_i w_i\quad\text{for all } i$$$

Lean4

theorem mulVec_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) : (diagonal v *ᵥ w) x = v x * w x :=
  diagonal_dotProduct v w x

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