inner_sum_right — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\langle x, \\sum_{i \\in s} y_i \\\\rangle_A = \\sum_{i \\in s} \\\\langle x, y_i \\\\rangle_A$$$

Lean4

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

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