sum_right — Mathlib

English

If t is a finite index set and B_i are bilinear forms, then the sum of B_i applied to a fixed pair equals the sum of the results: (∑ B_i) v w = ∑ B_i v w.

Русский

Пусть t является конечным индексным множеством и B_i — билинейные формы. Тогда сумма их применения к фиксированной паре равна сумме результатов: (∑ B_i) v w = ∑ B_i v w.

LaTeX

$$$$ \Big(\sum_{i\in t} B_i\Big)(v,w) = \sum_{i\in t} B_i(v,w). $$$$

Lean4

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

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