dotProduct_empty — Mathlib

English

Deprecated variant: the same empty-index dot product equality holds for Fin 0 → α.

Русский

Устаревшее формулирование той же равенства для функции на пустом индексе: Fin 0 → α.

LaTeX

$$$v : \\mathrm{Fin}\\,0 \\to \\alpha,\\ w : \\mathrm{Fin}\\,0 \\to \\alpha \\\\ v \\cdot w = 0$$$

Lean4

@[deprecated "Use Matrix.dotProduct_of_isEmpty instead." (since := "2025-09-07")]
theorem dotProduct_empty (v w : Fin 0 → α) : v ⬝ᵥ w = 0 :=
  Finset.sum_empty

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