English
Fix bases v1, v2. The map toLin provides a linear equivalence between the matrix space Mat(m,n,R) and the linear maps M1 → M2. This equivalence is invertible with inverse given by toMatrix.
Русский
Пусть заданы базисы v1, v2. Отображение toLin задаёт линейное эквидивное соответствие между пространством матриц Mat(m,n,R) и линейными отображениями M1 → M2. Это соответствие обратимо с обратной связью, заданной через toMatrix.
LaTeX
$$$\\text{toLin} : \\mathrm{Matrix}\; m\\; n\\; R \\ \\simeq_{R} (M_1 \\to_{R} M_2).$$$
Lean4
/-- Given bases of two modules `M₁` and `M₂` over a commutative ring `R`, we get a linear
equivalence between matrices over `R` indexed by the bases and linear maps `M₁ →ₗ M₂`. -/
def toLin : Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂ :=
(LinearMap.toMatrix v₁ v₂).symm
