toMatrix_map — Mathlib

English

A basis reindexing lemma: (b.reindex e).toMatrix v equals the submatrix of b.toMatrix v with rows permuted by e.

Русский

Лемма о переиндексации базы: (b.reindex e).toMatrix v равна подматрице той же матрицы, полученной перестановкой строк по e.

LaTeX

$$$ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (e.symm) id $$$

Lean4

@[simp]
theorem toMatrix_map (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) : (b.map f).toMatrix v = b.toMatrix (f.symm ∘ v) :=
  by
  ext
  simp only [toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]

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