Formal definition of $n$ by $0$ and $0$ by $n$ matrices

definitionmatrices

A matrix is usually informally defined as a rectangular array of numbers. To make this definition formal, we can define a matrix as a map from $$\{1,…,m\} \times \{1,…,n\}$$ to the underlying field of scalars, where $$\times$$ denotes cartesian product. However, a subtle complication arises when $$m=0$$ or $$n=0$$. In that case, the matrix would be an empty function. The problem, however, is that there is then no way to distinguish between $$m \times 0$$ matrices from $$0 \times n$$ matrices. In fact, under the cartesian product definition, for all natural numbers $$m$$, $$m'$$, $$n$$, and $$n'$$, the $$m \times 0$$, $$m' \times 0$$, $$0 \times n$$, and $$0 \times n'$$ matrices are all the same entity, namely the empty function. This is, to me, an undesirable state of affairs. I want to be able to distinguish, for example, $$2 \times 0$$, $$3 \times 0$$, $$0 \times 2$$, and $$0 \times 3$$ matrices. Is there a better definition of matrix that some mathematician has written about in some paper or book that avoids that problem?

A $$m\times n$$ matrix is a representation of a mapping from a $$n$$-dimensional vector space to a $$m$$-dimensional vector space. In that sense, a $$0\times m$$ matrix is different from a $$n\times 0$$ matrix. While they both represent the mapping we call "the zero mapping", the zero mappings are different mappings.
In other words, instead of speaking of mappings from $$\{1,\dots,m\}\times\{1,\dots,n\}$$, you can speak of linear maps from $$\mathbb F^n$$ to $$\mathbb F^m$$ (usually denoted something like $$\mathcal L(\mathbb F^n, \mathbb F^m)$$), and instead of speaking of a $$0\times m$$ matrix, you can speak of the element of $$\mathcal L(\mathbb F^0, \mathbb F^n)$$. That element (there is only one) is different from the element of $$\mathcal L(\mathbb F^m, \mathbb F^0)$$.