inner_right_fintype — Mathlib

English

For a Finite index type, the inner product ⟪v_i, ∑ j l_j v_j⟫ equals l_i for all i.

Русский

Для конечного индекса ⟪v_i, ∑ j l_j v_j⟫ = l_i для всех i.

LaTeX

$$$\forall i, \langle v_i, \sum_{j} l_j v_j \rangle = l_i$$$

Lean4

/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector. -/
theorem inner_right_fintype [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) :
    ⟪v i, ∑ i : ι, l i • v i⟫ = l i :=
  hv.inner_right_sum l (Finset.mem_univ _)

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