matPolyEquiv_eval — Mathlib

English

The coordinate-wise evaluation of matPolyEquiv M at r matches the evaluation of each entry polynomial at r.

Русский

По координатам: оценка по r каждого элемента матрицы после matPolyEquiv совпадает с оценкой каждого полинома в ячейке.

LaTeX

$$$(\\text{matPolyEquiv } M).\\mathrm{eval}(\\mathrm{scalar}\\; n\\; r)_{i j} = (M_{i j}).\\mathrm{eval}\\; r$$$

Lean4

theorem matPolyEquiv_eval (M : Matrix n n R[X]) (r : R) (i j : n) :
    (matPolyEquiv M).eval (scalar n r) i j = (M i j).eval r := by rw [matPolyEquiv_eval_eq_map, map_apply]

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