The main result of this section is theorem pmmpric, which shows that the ring of polynomial matrices and the ring of polynomials having matrices as coefficients (called "polynomials over matrices" in the following) are isomorphic:<br> <br><br> Or in a more common notation:<br> corresponds to M(n, R[t]), the ring of n x n polynomial matrices over the ring R.<br> corresponds to M(n, R)[t], the polynomial ring over the ring of n x n matrices with entries in ring R. <br><br> <br><br> with and ( i m j ) ) is an isomorphism between these rings:<br> <br> with (see pm2mpf1o and pm2mprngiso), and<br> <br> p ) <br><br> is the corresponding inverse function:<br> <br> (see mp2pm2mp). <br><br> In this section, the following conventions are mostly used: <ul> <li> is a (unital) ring (see df-ring)</li> <li> is the polynomial algebra over (the ring) (see df-ply1) <ul> <li> is its base set (see df-base)</li> <li> is its variable (see df-vr1)</li> <li> is its scalar multiplication (see df-vsca or lmodvscl)</li> <li> is its exponentiation (see df-mulg) </li> </ul></li> <li> is the algebra of N x N matrices over (the ring) (see df-mat)</li> <li> is the algebra of N x N matrices over (the polynomial ring) . <ul> <li> is its base set</li> <li> is a concrete polynomial matrix</li> </ul></li> <li> is the polynomial algebra over (the matrix ring) . <ul> <li> is its base set</li> <li> is a concrete polynomial with matrix coefficients</li> <li> is its variable</li> <li> is its scalar multiplication</li> <li> is its exponentiation</li></ul></li> </ul>