English
For a basis b of a semiring S over a ring R, the basis-induced matrix maps the vector-valued map to the corresponding coefficient vector via vecMul and dot product relations.
Русский
Для базиса b над полем S над кольцом R матричное отображение переводит вектор-отображение в вектор коэффициентов через vecMul и dot product.
LaTeX
$$b ᵥ* ((b.toMatrix v).map (algebraMap R S)) = v$$
Lean4
theorem toMatrix_map_vecMul {S : Type*} [Semiring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι' → S) :
b ᵥ* ((b.toMatrix v).map <| algebraMap R S) = v := by
ext i
simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def, sum_toMatrix_smul_self]