# Metamath Proof Explorer

According to Wikipedia ("Matrix (mathemetics)", 02-Apr-2019, https://en.wikipedia.org/wiki/Matrix_(mathematics)) "A matrix is a rectangular array of numbers or other mathematical objects for which operations such as addition and multiplication are defined. Most commonly, a matrix over a field F is a rectangular array of scalars each of which is a member of F. The numbers, symbols or expressions in the matrix are called its entries or its elements. The horizontal and vertical lines of entries in a matrix are called rows and columns, respectively.", and in the definition of [Lang] p. 503 "By an m x n matrix in [a commutative ring] R one means a doubly indexed family of elements of R, (aij), (i= 1,..., m and j = 1,... n) ... We call the elements aij the coefficients or components of the matrix. A 1 x n matrix is called a row vector (of dimension, or size, n) and a m x 1 matrix is called a column vector (of dimension, or size, m). In general, we say that (m,n) is the size of the matrix, ...". In contrast to these definitions, we denote any free module over a (not necessarily commutative) ring (in the meaning of df-frlm) with a Cartesian product as index set as "matrix". The two sets of the Cartesian product even need neither to be ordered or a range of (nonnegative/positive) integers nor finite. By this, the addition and scalar multiplication for matrices correspond to the addition (see frlmplusgval) and scalar multiplication (see frlmvscafval) for free modules. Actually, there isn't a definition for (arbitrary) matrices: Even the (general) matrix multiplication can be defined using functions from Cartesian products into a ring (which are elements of the base set of free modules), see df-mamu. By this, a statement like "Then the set of m x n matrices in R is a module (i.e., an R-module)" as in [Lang] p. 504 follows immediately from frlmlmod.

However, for square matrices there is the definition df-mat, defining the algebras of square matrices (of the same size over the same ring), extending the structure of the corresponding free module by the matrix multiplication as ring multiplication.

A "usual" matrix (aij), (i= 1,..., m and j = 1,... n) would be represented as element of (the base set of) , and a square matrix (aij), (i= 1,..., n and j = 1,... n) would be represented as element of (the base set of) .

Finally, it should be mentioned that our definitions of matrices include the zero-dimensional cases, which is excluded in the definition of many authors, e.g. in [Lang] p. 503. It is shown in mat0dimbas0 that the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). The determinant is also defined for such an empty matrix, see mdet0pr.

1. The matrix multiplication
2. Square matrices
3. The matrix algebra
4. Matrices of dimension 0 and 1
5. The subalgebras of diagonal and scalar matrices
6. Multiplication of a matrix with a "column vector"
7. Replacement functions for a square matrix
8. Submatrices