English
Evaluating a polynomial-matrix via matPolyEquiv.symm corresponds to evaluating the original matrix M with the scalar action scalar n r.
Русский
Строка оценки полиномиально-матрицеской формы через matPolyEquiv.symm соответствует оценке исходной матрицы M скалярным действием scalar n r.
LaTeX
$$$(\\mathrm{matPolyEquiv}.\\mathrm{symm}\\ M).map(\\mathrm{eval}\\ r) = M.\\mathrm{eval}(\\mathrm{scalar}\\; n\\; r)$$$
Lean4
theorem matPolyEquiv_symm_map_eval (M : (Matrix n n R)[X]) (r : R) :
(matPolyEquiv.symm M).map (eval r) = M.eval (scalar n r) :=
by
suffices
((aeval r).mapMatrix.comp matPolyEquiv.symm.toAlgHom : (Matrix n n R)[X] →ₐ[R] _) =
(eval₂AlgHom' (AlgHom.id R _) (scalar n r) fun x => (scalar_commute _ (Commute.all _) _).symm)
from DFunLike.congr_fun this M
ext : 1
· ext M : 1
simp [Function.comp_def]
· simp
