English
If MM' = 1 then for any x ∈ M1, applying Matrix.toLin v1 v2 M then Matrix.toLin v2 v1 M' yields x, and similarly for the opposite order; i.e., the inverse maps compose to the identity on M1 and M2.
Русский
Если MM' = 1, то для любого x ∈ M1 применение Matrix.toLin v1 v2 M затем Matrix.toLin v2 v1 M' возвращает x, и в противоположном порядке также; т.е. обратные отображения образуют тождество.
LaTeX
$$$\big( \mathrm{toLin}_{v_2,v_1}(M') \circ \mathrm{toLin}_{v_1,v_2}(M) \big)(x) = x$ and $\big( \mathrm{toLin}_{v_1,v_2}(M) \circ \mathrm{toLin}_{v_2,v_1}(M') \big)(y) = y$$$
Lean4
/-- Given a basis of a module `M₁` over a commutative ring `R`, we get an algebra
equivalence between linear maps `M₁ →ₗ M₁` and square matrices over `R` indexed by the basis. -/
def toMatrixAlgEquiv : (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R :=
AlgEquiv.ofLinearEquiv (LinearMap.toMatrix v₁ v₁) (LinearMap.toMatrix_one v₁) (LinearMap.toMatrix_mul v₁)
