English
If basis is reindexed by an equivalence, the corresponding matrix is obtained by applying the corresponding submatrix reindexing.
Русский
Если база переиндексируется по эквивалентности, соответствующая матрица получена применением перестановки индексов
LaTeX
$$$ (b.reindex\ e).toMatrix\ v = Matrix.reindexAlgEquiv R R\ e\ (b.toMatrix (v \circ e)) $$$
Lean4
/-- See also `Basis.toMatrix_reindex` which gives the `simp` normal form of this result. -/
theorem toMatrix_reindex' [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
(b.reindex e).toMatrix v = Matrix.reindexAlgEquiv R R e (b.toMatrix (v ∘ e)) :=
by
ext
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply, Matrix.reindex_apply,
Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply, Finsupp.mapDomain_equiv_apply]
