dotProduct_single_one — Mathlib

English

Let v be a function from n to α and i be an element of n. Then the dot product of v with the i-th standard basis vector e_i equals v(i).

Русский

Пусть v: n → α и i ∈ n. Тогда скалярное произведение вектора v с i-ым базисным вектором e_i равно v(i).

LaTeX

$$$ v \cdot e_i = v_i $$$

Lean4

theorem dotProduct_single_one [DecidableEq n] (v : n → α) (i : n) : v ⬝ᵥ Pi.single i 1 = v i := by
  rw [dotProduct_single, mul_one]

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