inner_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- An inner product with a sum on the right. -/
theorem inner_sum {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) : ⟪x, ∑ i ∈ s, f i⟫ = ∑ i ∈ s, ⟪x, f i⟫ :=
  map_sum (LinearMap.flip sesqFormOfInner x) _ _

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