This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.
Some results are proved about the linear map corresponding to a diagonal matrix (range, ker and rank).
to_lin, to_matrix, lin_equiv_matrix
linear_map, matrix, linear_equiv, diagonal
Evaluation of matrices gives a linear map from matrix m n R to linear maps (n → R) →ₗ[R] (m → R).
Evaluation of matrices gives a map from matrix m n R to linear maps (n → R) →ₗ[R] (m → R).
The linear map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R.
The map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R.
to_lin is the left inverse of to_matrix.
to_lin is the right inverse of to_matrix.
Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.
Given a basis 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.