sum_inner — Mathlib

English

An inner product with a right sum: ⟪x, ∑i∈s f_i⟫ = ∑i∈s ⟪x, f_i⟫.

Русский

Сумма справа векторного аргумента: ⟪x, ∑i∈s f_i⟫ = ∑i∈s ⟪x, f_i⟫.

LaTeX

$$$\langle x, \sum_{i\in s} f_i\rangle = \sum_{i\in s} \langle x, f_i\rangle$$$

Lean4

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

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