toMatrix_map_vecMul — Mathlib

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]

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