sum_left — Mathlib

English

For a finite index set t, a family of vectors g(i) ∈ M, and v ∈ M, the bilinear form is additive in the right argument: B(v, ∑_{i∈t} g(i)) = ∑_{i∈t} B(v, g(i)).

Русский

Для конечного множества индексов t и функций g: t → M, верно: B(v, ∑_{i∈t} g(i)) = ∑_{i∈t} B(v, g(i)).

LaTeX

$$$$ B(v, \sum_{i\in t} g(i)) = \sum_{i\in t} B(v, g(i)). $$$$

Lean4

theorem sum_left {α} (t : Finset α) (g : α → M) (w : M) : B (∑ i ∈ t, g i) w = ∑ i ∈ t, B (g i) w :=
  B.map_sum₂ t g w

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