sum_dotProduct — Mathlib

English

Re-statement of dotProduct with PUnit: dotProduct(v,w) = v(PUnit.unit) · w(PUnit.unit).

Русский

Повторение выражения dotProduct для PUnit: dotProduct(v,w) = v(ед.) · w(ед.) .

LaTeX

$$$$ \operatorname{dotProduct}(v, w) = v(\ast) \cdot w(\ast). $$$$

Lean4

theorem sum_dotProduct {ι : Type*} (s : Finset ι) (u : ι → (m → α)) (v : m → α) :
    (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v :=
  by
  simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]
  rw [Finset.sum_comm]

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