vecMul_diagonal

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#Matrix.vecMul_diagonal

English

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

Русский

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

LaTeX

$$$(v \; \mathrm{vecMul} \; \mathrm{diag}(w))_i = v_i w_i$$$

Lean4

theorem vecMul_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) : (v ᵥ* diagonal w) x = v x * w x :=
  dotProduct_diagonal' v w x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru