sum_apply — Mathlib

English

For a finite t and B_i: BilinForm, the evaluation on v,w commutes with summation: ∑ B_i v w = (∑ B_i) v w.

Русский

Для конечного t и B_i: BilinForm, вычисление на v,w коммутирует суммированию: ∑ B_i(v,w) = (∑ B_i)(v,w).

LaTeX

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

Lean4

theorem sum_apply {α} (t : Finset α) (B : α → BilinForm R M) (v w : M) : (∑ i ∈ t, B i) v w = ∑ i ∈ t, B i v w := by
  simp only [coeFn_sum, Finset.sum_apply]

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