toMatrix_reindex — Mathlib

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]

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