zero_dotProduct' — Mathlib

English

For any finite index set, the dot product of the zero vector with any vector v is zero: ∑i 0 · v(i) = 0.

Русский

Для любого конечного множества индексов скалярное произведение нулевого вектора с любым вектором v равняется нулю: ∑i 0 · v(i) = 0.

LaTeX

$$$\sum_{i} 0 \cdot v_i = 0$$$

Lean4

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

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