Algebra isomorphism between matrices of polynomials and polynomials of matrices
[comm_ring R] [ring A] [algebra R A]
polynomial A ≃ₐ[R] (A ⊗[R] polynomial R).
Combining this with the isomorphism
matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) proved earlier
ring_theory.matrix_algebra, we obtain the algebra isomorphism
which is characterized by
coeff (mat_poly_equiv m) k i j = coeff (m i j) k
We will use this algebra isomorphism to prove the Cayley-Hamilton theorem.
The algebra isomorphism stating "matrices of polynomials are the same as polynomials of matrices".
(You probably shouldn't attempt to use this underlying definition ---
it's an algebra equivalence, and characterised extensionally by the lemma