English
If we reindex the basis v1 by a permutation that preserves the range (i.e., v1.reindexRange), then the matrix obtained from f with respect to the reindexed basis equals the original matrix with indices permuted correspondingly: toMatrixAlgEquiv v1.reindexRange f ⟨v1 k, _⟩ ⟨v1 i, _⟩ = toMatrixAlgEquiv v1 f k i.
Русский
Если переиндексировать базис v1 посредством перестановки, сохраняющей диапазон, то матрица отображения f относительно переиндексированного базиса равна исходной матрице со соответствующим перестановочным изменением индексов: toMatrixAlgEquiv v1.reindexRange f ... = toMatrixAlgEquiv v1 f k i.
LaTeX
$$$\mathrm{toMatrixAlgEquiv}_{v_1.reindexRange} f \langle \mathrm{Module.Basis.instFunLike.coe}
v_1 k, \cdots \rangle \langle \mathrm{Module.Basis.instFunLike.coe}
v_1 i, \cdots \rangle = \mathrm{toMatrixAlgEquiv}_{v_1} f k i$$$
Lean4
theorem toMatrixAlgEquiv_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
LinearMap.toMatrixAlgEquiv v₁.reindexRange f ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
LinearMap.toMatrixAlgEquiv v₁ f k i :=
by simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
