inner_sum — Mathlib

English

The real and complex inner product on DFinsupp respects sum on the left: ⟪l.sum f, x⟫ = ∑ ⟪f_i, x⟫.

Русский

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

LaTeX

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

Lean4

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

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