English
The two fundamental functors between endomorphisms and square matrices are mutually inverse: Matrix.toLinAlgEquiv and LinearMap.toMatrixAlgEquiv are inverses of each other up to the natural isomorphism.
Русский
Два основных отображения между концевыми отображениями и квадратными матрицами являются взаимно обратными: Matrix.toLinAlgEquiv и LinearMap.toMatrixAlgEquiv взаимно обратны на уровне естественных изоморфизмов.
LaTeX
$$$\mathrm{toLinAlgEquiv}_{v_1} \circ \mathrm{toMatrixAlgEquiv}_{v_1} = \mathrm{id}$ and $\mathrm{toMatrixAlgEquiv}_{v_1} \circ \mathrm{toLinAlgEquiv}_{v_1} = \mathrm{id}$$$
Lean4
theorem toMatrixAlgEquiv_apply' (f : M₁ →ₗ[R] M₁) (i j : n) :
LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i :=
LinearMap.toMatrixAlgEquiv_apply v₁ f i j
