sum_repr — Mathlib

English

For a finite-index basis B of M, the vector u is reconstructed by summing the i-th coordinate of u with respect to the basis: ∑ i, b.repr u i • b i = u.

Русский

Для конечного индекса базиса B модуля M вектор u восстанавливается суммой по координатам: ∑ i, b.repr u i • b i = u.

LaTeX

$$$$ \sum_i b.repr\,u\,i \cdot b_i = u $$$$

Lean4

@[simp]
theorem sum_repr [Fintype ι] (b : Basis ι R M) (u : M) : ∑ i, b.repr u i • b i = u :=
  b.sum_equivFun u

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