mathlib

ba8af8cb - feat(ring_theory/polynomial_algebra): polynomial A ≃ₐ[R] (A ⊗[R] polynomial R) (#3275)

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 ``` Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jalex Stark <alexmaplegm@gmail.com> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>