inner_sum_left — Mathlib

English

For any finite set s, ⟪∑_{i∈s} x_i, y⟫ = ∑_{i∈s} ⟪x_i, y⟫.

Русский

Для любого конечного множества s: ⟪∑_{i∈s} x_i, y⟫ = ∑_{i∈s} ⟪x_i, y⟫.

LaTeX

$$$\\\\langle \\sum_{i \\in s} x_i, y \\\\rangle_A = \\sum_{i \\in s} \\\\langle x_i, y \\\\rangle_A$$$

Lean4

@[simp]
theorem inner_sum_left {ι : Type*} {s : Finset ι} {x : ι → E} {y : E} : ⟪∑ i ∈ s, x i, y⟫ = ∑ i ∈ s, ⟪x i, y⟫ :=
  map_sum (innerₛₗ.flip y) ..

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