dotProduct_zero'

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#dotProduct_zero'

English

The dot product of a vector with the zero function is zero (renamed variant).

Русский

Скалярное произведение вектора с нулевой функцией равно нулю (вариант названия).

LaTeX

$$$$\operatorname{dotProduct}(v,0) = 0.$$$$

Lean4

@[simp]
theorem dotProduct_zero' : (v ⬝ᵥ fun _ => 0) = 0 :=
  dotProduct_zero v

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

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

Разделы

Аффилиация

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