English
There is a canonical algebra isomorphism stating that matrices whose entries are polynomials in R[X] correspond to polynomials with matrix coefficients, i.e., Matrix n n R[X] is isomorphic to (Matrix n n R)[X].
Русский
Существует каноническое алгебраическое изоморфизм, утверждающий, что матрицы со степенями X в записях эквивалентны полиномам со значениями в матрицах: Matrix n n R[X] ≅ (Matrix n n R)[X].
LaTeX
$$$\\text{matPolyEquiv} :\\; \\mathrm{Matrix}_{n\\times n}(\\mathbb{R}[X]) \\simeq_{\\mathbb{R}} (\\mathrm{Matrix}_{n\\times n}(\\mathbb{R}))[X]$$$
Lean4
/-- 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
`matPolyEquiv_coeff_apply` below.)
-/
noncomputable def matPolyEquiv : Matrix n n R[X] ≃ₐ[R] (Matrix n n R)[X] :=
((matrixEquivTensor n R R[X]).trans (Algebra.TensorProduct.comm R _ _)).trans (polyEquivTensor R (Matrix n n R)).symm
