diagonal_dotProduct — Mathlib

English

A second formulation: sumElim dotProduct distributes over sums in a more general setting of sums over a Finset.

Русский

Вторая формулировка: сумма в dotProduct распределяется над суммами в более общем виде.

LaTeX

$$$$ \operatorname{dotProduct}\bigl( s. sum (\lambda i, u_i), v \bigr) = \sum_{i \in s} \operatorname{dotProduct}(u_i, v). $$$$

Lean4

@[simp]
theorem diagonal_dotProduct (i : m) : diagonal v i ⬝ᵥ w = v i * w i :=
  by
  have : ∀ j ≠ i, diagonal v i j * w j = 0 := fun j hij => by simp [diagonal_apply_ne' _ hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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