English
The canonical equivalence between M and functions on ι preserves left inverse structure and expresses the expansion as a finite sum.
Русский
Каноническая эквивалентность между M и функциями на ι сохраняет структуру левых обратных и выражает разложение в виде конечной суммы.
LaTeX
$$$b.equivFun.symm x = \sum_i x_i b_i$ and $b.repr (\sum_i x_i b_i) = x$$$
Lean4
/-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
@[simp]
theorem equivFun_symm_apply [Fintype ι] (b : Basis ι R M) (x : ι → R) : b.equivFun.symm x = ∑ i, x i • b i := by
simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]
