one_dotProduct

Mathlib.Data.Matrix.Mul

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

English

The dot product with the constant-one is symmetric to the addition: dotProduct(1, v) = ∑ i v(i).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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