English
For a matrix M ∈ Mat_{n×n}(R) and a vector v ∈ M1, the image under the linear map Matrix.toLinAlgEquiv v1 M is the sum over j of the j-th coordinate of M written in the v1-coordinates times the j-th basis vector v1_j.
Русский
Для матрицы M и вектора v ∈ M1 образ линейного отображения Matrix.toLinAlgEquiv v1 M равен сумме по j координат M в базисе v1, умноженных на вектор v1_j.
LaTeX
$$$\mathrm{toLinAlgEquiv}_{v_1}(M)(v) = \sum_j (M *^v v_1.repr v)_j \; v_{1,j}$$$
Lean4
/-- Given a basis of a module `M₁` over a commutative ring `R`, we get an algebra
equivalence between square matrices over `R` indexed by the basis and linear maps `M₁ →ₗ M₁`. -/
def toLinAlgEquiv : Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁ :=
(LinearMap.toMatrixAlgEquiv v₁).symm
