vec2_dotProduct

Mathlib.LinearAlgebra.Matrix.Notation

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

English

The dot product of 2-element vectors is v0 w0 + v1 w1.

Русский

Скалярное произведение векторов длины 2 равно v0 w0 + v1 w1.

LaTeX

$$$v \cdot w = v_0 w_0 + v_1 w_1$$$

Lean4

@[simp]
theorem vec2_dotProduct (v w : Fin 2 → α) : v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1 :=
  vec2_dotProduct'

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

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

Разделы

Аффилиация

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