English
Reindexing a basis by an equivalence e translates to a corresponding reindexing of the matrix by the same equivalence.
Русский
Переиндексация базиса по эквивалентности e соответствует аналогичной переиндексации матрицы.
LaTeX
$$$ (b.reindex e).toMatrix v = Matrix.reindexAlgEquiv e (b.toMatrix (v \circ e)) $$$
Lean4
@[simp]
theorem toMatrix_reindex (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
(b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id :=
by
ext
simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id, Finsupp.mapDomain_equiv_apply]