sum_inner — Mathlib

English

In DFinsupp, inner product with a sum is the sum of inner products: ⟪l.sum f, x⟫ = ∑ a ⟪f a, x⟫.

Русский

В DFinsupp скалярное произведение с суммой равно сумме скалярных произведений: ⟪l.sum f, x⟫ = ∑ a ⟪f a, x⟫.

LaTeX

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

Lean4

protected theorem sum_inner {ι : Type*} [DecidableEq ι] {α : ι → Type*} [∀ i, AddZeroClass (α i)]
    [∀ (i) (x : α i), Decidable (x ≠ 0)] (f : ∀ i, α i → E) (l : Π₀ i, α i) (x : E) :
    ⟪l.sum f, x⟫ = l.sum fun i a => ⟪f i a, x⟫ := by simp +contextual only [DFinsupp.sum, sum_inner]

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