vec3_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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