English
For any i, the i-th coordinate of repr.symm f recovers the coefficient f i for any finitely supported f: b.coord i (b.repr.symm f) = f i.
Русский
Для любого i координата i-й компоненты в выражении repr.symm f восстанавливает коэффициент f i: b.coord i (b.repr.symm f) = f i.
LaTeX
$$$ b.coord\,i\ (b.repr.symm\ f) = f(i) $$$
Lean4
theorem coord_repr_symm (b : Basis ι R M) (i : ι) (f : ι →₀ R) : b.coord i (b.repr.symm f) = f i := by
simp only [repr_symm_apply, coord_apply, repr_linearCombination]