Commit 2020-07-08 14:31 ba8af8cbView 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