English
For a finite index set, given l : ι →₀ R and i ∈ ι, the i-th coordinate of the linear combination of basis vectors with coefficients l is l i; i.e., Finsupp.linearCombination R b.coord l (b i) = l i.
Русский
Для конечного множества индексов и заданного l : ι →₀ R, i : ι, линейная комбинация координат по базису даёт i-ю координату l, то есть Finsupp.linearCombination R b.coord l (b i) = l i.
LaTeX
$$$ Finsupp.linearCombination R\\, b.coord\\, l\\, (b i) = l i $$$
Lean4
/-- `simp` normal form version of `linearCombination_dualBasis` -/
@[simp]
theorem linearCombination_coord [Finite ι] (b : Basis ι R M) (f : ι →₀ R) (i : ι) :
Finsupp.linearCombination R b.coord f (b i) = f i :=
by
haveI := Classical.decEq ι
rw [← coe_dualBasis, linearCombination_dualBasis]
