sum_equivFun — Mathlib

English

Let B be a finite-index basis of M over R and u ∈ M. The sum over i of the i-th coordinate times the i-th basis vector equals u: ∑ i, b.equivFun u i • b i = u.

Русский

Пусть B — база M над R индексированная скольким-то конечным множеством ι и возьмём вектор u ∈ M. Тогда u можно разложить по базису как сумма ∑_i b_i · coord_i, то есть ∑ i, b.equivFun u i • b i = u.

LaTeX

$$$$ \sum_i (b.equivFun\, u\, i)\cdot b_i = u $$$$

Lean4

theorem sum_equivFun [Fintype ι] (b : Basis ι R M) (u : M) : ∑ i, b.equivFun u i • b i = u := by
  rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]

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