Commit 2020-07-08 14:31 ba8af8cb

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