single_dotProduct — Mathlib

English

For a basis vector at i with weight x, dotProduct(Pi.single i x, v) = v(i) x.

Русский

Для базисного вектора Pi.single i x скалярное произведение с v равно v(i) x.

LaTeX

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

Lean4

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

  have : ∀ j ≠ i, (Pi.single i x : m → α) j * v 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

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