vec2_dotProduct'

Mathlib.LinearAlgebra.Matrix.Notation

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

English

The dashed dot product of 2-element vectors is equal to a0 b0 + a1 b1.

Русский

Усечённое скалярное произведение векторов длины 2 равно a0 b0 + a1 b1.

LaTeX

$$$\begin{pmatrix} a_0 \\ a_1 \end{pmatrix} \cdot' \begin{pmatrix} b_0 \\ b_1 \end{pmatrix} = a_0 b_0 + a_1 b_1$$$

Lean4

theorem vec2_dotProduct' {a₀ a₁ b₀ b₁ : α} : ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁ := by simp

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

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

Разделы

Аффилиация

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