English
Changing the indexing (reindexing) of an orthonormal basis corresponds to reindexing the associated matrix representation consistently on both domain and codomain sides.
Русский
Изменение индексирования ортонормированного базиса соответствует корректному перенумеровке матричного представления отображения как в области, так и в кодоме.
LaTeX
$$$toMatrixOrthonormal (v_1.reindex e) f = (toMatrixOrthonormal v_1 f).reindex e e$$$
Lean4
theorem toMatrixOrthonormal_reindex (e : n ≃ m) (f : E →ₗ[𝕜] E) :
toMatrixOrthonormal (v₁.reindex e) f = (toMatrixOrthonormal v₁ f).reindex e e :=
Matrix.ext fun i j =>
calc
toMatrixOrthonormal (v₁.reindex e) f i j
_ = (v₁.reindex e).repr (f (v₁.reindex e j)) i := f.toMatrix_apply ..
_ = v₁.repr (f (v₁ (e.symm j))) (e.symm i) := by simp
_ = toMatrixOrthonormal v₁ f (e.symm i) (e.symm j) := Eq.symm (f.toMatrix_apply ..)
