A polynomial matrix or matrix of polynomials is a matrix whose elements
are univariate (or multivariate) polynomials. See Wikipedia "Polynomial
matrix" https://en.wikipedia.org/wiki/Polynomial_matrix (18-Nov-2019). In
this section, only square matrices whose elements are univariate polynomials
are considered. Usually, the ring of such matrices, the ring of n x n
matrices over the polynomial ring over a ring , is denoted by
M(n, R[t]). The elements of this ring are called "polynomial matrices (over
the ring )" in the following. In Metamath notation, this ring is
defined by , usually represented by the class
variable (or , if is already occupied):
with .