vec3_dotProduct' — Mathlib

English

The dashed dot product of 3-element vectors: a0 b0 + a1 b1 + a2 b2.

Русский

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

LaTeX

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

Lean4

theorem vec3_dotProduct' {a₀ a₁ a₂ b₀ b₁ b₂ : α} : ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂ := by
  simp [add_assoc]
    -- This is not tagged `@[simp]` because it does not mesh well with simp lemmas for
    -- dot and cross products in dimension 3.

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