single_one_dotProduct

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#single_one_dotProduct

English

Let i ∈ n and v: n → α. Then the dot product of the i-th basis vector with v equals v(i).

Русский

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

LaTeX

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

Lean4

theorem single_one_dotProduct [DecidableEq n] (i : n) (v : n → α) : Pi.single i 1 ⬝ᵥ v = v i := by
  rw [single_dotProduct, one_mul]

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

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

Разделы

Аффилиация

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