dotProduct_diagonal — Mathlib

English

The dot product of a vector with a diagonal matrix with diagonal entries w is given by (v ⬝ᵥ Diagonal(w))_i = v_i w_i.

Русский

Скалярное произведение вектора с диагональной матрицей имеет вид (v ⬝ᵥ Diagonal(w))_i = v_i w_i.

LaTeX

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

Lean4

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

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