dotProduct_single — Mathlib

English

A variant of the previous: dotProduct(v, Pi.single i x) = v(i) x.

Русский

Вариант предыдущего: dotProduct(v, Pi.single i x) = v(i) x.

LaTeX

$$$$ \operatorname{dotProduct}(v, \operatorname{Pi.single} i x) = v(i) \cdot x. $$$$

Lean4

@[simp]
theorem dotProduct_single (x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x := by
  -- Porting note: added `(_ : m → α)`

  have : ∀ j ≠ i, v j * (Pi.single i x : m → α) j = 0 := fun j hij => by simp [Pi.single_eq_of_ne hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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