inner_sum — Mathlib

English

The left-right inner product commutes with scalar sums in Finsupp form: ⟪x, l.sum a • v a⟫ = ∑ a conj(a) ⟪x, v a⟫.

Русский

Левая линейность для Finsupp: ⟪x, l.sum a • v a⟫ = ∑ a conj(a) ⟪x, v a⟫.

LaTeX

$$$\langle x, \sum_{i} a_i v_i \rangle = \sum_{i} a_i \langle x, v_i \rangle$$$

Lean4

/-- An inner product with a sum on the right, `Finsupp` version. -/
protected theorem inner_sum {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
    ⟪x, l.sum fun (i : ι) (a : 𝕜) => a • v i⟫ = l.sum fun (i : ι) (a : 𝕜) => a • ⟪x, v i⟫ :=
  by
  convert inner_sum (𝕜 := 𝕜) l.support (fun a => l a • v a) x
  simp only [inner_smul_right, Finsupp.sum, smul_eq_mul]

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