Linear map of a matrix

Definition

Let $F$ be a field, and let $V$ and $W$ be vector spaces over $F$ with bases $B = (b_1, \dots, b_n)$ and $C = (c_1, \dots, c_m)$. Let $A = (a_{ij})$ be an $m \times n$ matrix over $F$. The linear map of $A$ in the bases $B$ and $C$ is the linear map $T_A \colon V \to W$ with $$T_A(b_j) = \sum_{i=1}^{m} a_{ij} c_i \qquad (1 \le j \le n).$$

Remarks

The map $A \mapsto T_A$ is the inverse of the map $T \mapsto [T]_{C,B}$ of the matrix of a linear map. For $V = F^n$ and $W = F^m$ with the standard bases, $T_A$ is the map $x \mapsto Ax$, see multiplication by a matrix as a linear map. In Mathlib, this map is Matrix.toLin.

Explanations

L1 human

A matrix and two bases together define a linear map. Column $j$ tells us where the map sends basis vector $j$. This undoes the step from a linear map to its matrix.