dotProductᵣ_eq — Mathlib

English

For any a,b, dotProductᵣ a b equals the standard dot product a · b.

Русский

Для любых a, b выполняется равенство dotProductᵣ a b = a · b.

LaTeX

$$$\\text{dotProduct}ᵣ(a,b) = a \\cdot b$$$

Lean4

/-- This can be used to prove
```lean
example (a b c d : α) [Mul α] [AddCommMonoid α] :
  dot_product ![a, b] ![c, d] = a * c + b * d :=
(dot_productᵣ_eq _ _).symm
```
-/
@[simp]
theorem dotProductᵣ_eq [Mul α] [AddCommMonoid α] {m} (a b : Fin m → α) : dotProductᵣ a b = a ⬝ᵥ b := by
  simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq, Function.comp_apply]

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