vec2_add — Mathlib

English

Addition of 2-element vectors is done componentwise: [a0,a1] + [b0,b1] = [a0+b0, a1+b1].

Русский

Сложение векторов длины 2 выполняется по компонентам: [a0,a1] + [b0,b1] = [a0+b0, a1+b1].

LaTeX

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

Lean4

theorem vec2_add [Add α] (a₀ a₁ b₀ b₁ : α) : ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] := by simp

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