dotProduct_of_isEmpty

Mathlib.LinearAlgebra.Matrix.Notation

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

English

If the indexing set is empty, the dot product of two functions is zero.

Русский

Если индексное множество пусто, скалярное произведение двух функций равно нулю.

LaTeX

$$$v \\cdot w = 0$$$

Lean4

@[simp]
theorem dotProduct_of_isEmpty [Fintype n'] [IsEmpty n'] (v w : n' → α) : v ⬝ᵥ w = 0 :=
  Finset.sum_of_isEmpty _

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

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

Разделы

Аффилиация

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