dotProduct_diagonal' — Mathlib

English

Dual version: dotProduct(v, Diagonal(w) i) = v(i) w(i).

Русский

Двойная версия: dotProduct(v, Diagonal(w) i) = v(i) w(i).

LaTeX

$$$$ \operatorname{dotProduct}\bigl(v, \operatorname{diagonal}(w)\, i\bigr) = v(i) \cdot w(i). $$$$

Lean4

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

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