English
For fixed bases v1 of M1 and v2 of M2, the map toMatrix defines a linear isomorphism between the space of linear maps M1 → M2 and the space of matrices with entries in R indexed by m and n.
Русский
Для фиксированных базисов v1 и v2 отображение toMatrix задаёт линейное изоморфизм между пространством линейных отображений M1 → M2 и пространством матриц над R размером m×n, индексированным по данным базисам.
LaTeX
$$$\\text{toMatrix}_{v_1,v_2} : (M_1 \\to_{R} M_2) \\ \\cong_{R} \\mathrm{Matrix}\; m\\; n\\; R.$$$
Lean4
/-- Given bases of two modules `M₁` and `M₂` over a commutative ring `R`, we get a linear
equivalence between linear maps `M₁ →ₗ M₂` and matrices over `R` indexed by the bases. -/
def toMatrix : (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R :=
LinearEquiv.trans (LinearEquiv.arrowCongr v₁.equivFun v₂.equivFun) LinearMap.toMatrix'
