Linear Algebra over a Ring/Multilinear algebra

Definition (multilinear function):

Let $R$ be a ring, and let $M_{1},\ldots ,M_{n},K$ be $R$-modules. Then the set of $R$-multilinear functions from $M_{1}\times \cdots \times M_{n}$ to $K$ is the set

Failed to parse (unknown function "\middle"): {\displaystyle L(M_1, \ldots, M_n, K) := \left\{ f: M_1 \times M_n \to K \middle| \forall j \in [n]: \forall m_1 \in M_1, \ldots, m_n \in M_n, l_j \in M_j, r \in R: f(m_1, \ldots, m_j + r l_j, \ldots, \right\}} .

Proposition (equivalent definition of tensor product of free modules using multilinear functions):

Let $R$ be a ring, and let $M_{1},\ldots ,M_{n}$ be free, finitely generated $R$-modules. Then if we alternatively define

$M_{1}^{*}\otimes \cdots \otimes M_{n}^{*}:=L(M_{1},\ldots ,M_{n},R)$,

and let the elementary tensors be $m_{1}^{*}\otimes \cdots \otimes m_{n}^{*}(l_{1},\ldots ,l_{n}):=m_{1}^{*}(l_{1})\cdots m_{n}^{*}(l_{n})$, then the $M_{1}\otimes M_{n}$ from this definition satisfies the same universal property as the usual tensor product $M_{1}\otimes \cdots \otimes M_{n}$. In particular, the two tensor products are canonically isomorphic.

Proof: For $j\in [n]$, let $(e_{\lambda }^{j})_{\lambda \in \Lambda _{j}}$ be a basis of $M_{j}$, where $\Lambda _{j}$ is the respective finite index set. Given any $R$-module $K$ and any multilinear map $f:M_{1}\times \cdots \times M_{n}\to K$, we want a unique linear function $g:M_{1}\otimes \cdots \otimes M_{n}\to K$ such that $g\circ h=f$, where $h:M_{1}\times \cdots \times M_{n}\to M_{1}^{*}\otimes \cdots \otimes M_{n}^{*}$ is the map that sends a tuple to the respective elementary tensor. $\Box$