English
There is an algebra equivalence between endomorphisms of M1 and square matrices indexed by a basis, and this equivalence behaves compatibly with the Lin-to-Matrix correspondence; applying the equivalence to a linear map f yields the corresponding matrix, and vice versa.
Русский
Существует алгебраическая эквиваличность между концевыми отображениями M1 и квадратными матрицами, индексированными базисом, и эта эквивалентность совместима с соответствием между линейным отображением и матрицей; применение эквивалентности к f даёт соответствующую матрицу и наоборот.
LaTeX
$$$\mathrm{toLinAlgEquiv}_{v_1}(M) \cong \mathrm{toMatrixAlgEquiv}_{v_1}(f)$ и аналогично в обратную сторону$$
Lean4
@[simp]
theorem toMatrixAlgEquiv_toLinAlgEquiv (M : Matrix n n R) :
LinearMap.toMatrixAlgEquiv v₁ (Matrix.toLinAlgEquiv v₁ M) = M := by
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]
