matPolyEquiv_eval_eq_map — Mathlib

English

Evaluating matPolyEquiv M at X with r corresponds to applying the coefficient-wise map of M via eval r.

Русский

Оценка matPolyEquiv M в X эквивалентна применению коэффициентно-отображения M через eval r.

LaTeX

$$$(\\mathrm{matPolyEquiv} \\ M).\\mathrm{eval}(\\mathrm{scalar}\\; n\\; r) = M.map(\\mathrm{eval}\\ r)$$$

Lean4

theorem matPolyEquiv_eval_eq_map (M : Matrix n n R[X]) (r : R) : (matPolyEquiv M).eval (scalar n r) = M.map (eval r) :=
  by simpa only [AlgEquiv.symm_apply_apply] using (matPolyEquiv_symm_map_eval (matPolyEquiv M) r).symm

Похожие утверждения