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

$L(M_{1},\ldots ,M_{n},K):=\left\{f:M_{1}\times M_{n}\to K|\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}+rl_{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$