dotProduct_one

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#dotProduct_one

English

The dot product with the constant-one function equals the sum of the entries: dotProduct(v, 1) = ∑ i v(i).

Русский

Скалярное произведение с константой 1 даёт сумму компонент: dotProduct(v, 1) = ∑ i v(i).

LaTeX

$$$$\operatorname{dotProduct}(v,1) = \sum_{i} v(i).$$$$

Lean4

theorem dotProduct_one (v : n → α) : v ⬝ᵥ 1 = ∑ i, v i := by simp [(· ⬝ᵥ ·)]

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

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

Разделы

Аффилиация

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