inner_right_finsupp — Mathlib

English

In an orthonormal family, the inner product with a FinSupp linear combination yields the coefficient: ⟪v_i, linearCombination 𝕜 v l⟫ = l_i.

Русский

Для ортонормированного семейства скалярное произведение с линейной комбинацией по Finsupp дает коэффициент: ⟪v_i, linearCombination 𝕜 v l⟫ = l_i.

LaTeX

$$$\langle v_i, \operatorname{linearCombination} 𝕜 v l \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_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
    ⟪v i, linearCombination 𝕜 v l⟫ = l i := by
  classical simpa [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv] using Eq.symm

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