# Commit 2020-07-08 14:31 ba8af8cb

View on Github →feat(ring_theory/polynomial_algebra): polynomial A ≃ₐ[R] (A ⊗[R] polynomial R) (#3275)
This is a formal nonsense preliminary to the Cayley-Hamilton theorem, which comes in the next PR.
We produce the algebra isomorphism `polynomial A ≃ₐ[R] (A ⊗[R] polynomial R)`

, and as a consequence also the algebra isomorphism

```
matrix n n (polynomial R) ≃ₐ[R] polynomial (matrix n n R)
```

which is characterized by

```
coeff (matrix_polynomial_equiv_polynomial_matrix m) k i j = coeff (m i j) k
```