eval_toMvPolynomial — Mathlib

English

Evaluating after embedding and then evaluating at a point is the same as evaluating the original polynomial at the corresponding image point.

Русский

Оценивание после вложения и последующего подстановочного значения эквивалентно оцениванию исходного полинома в соответствующем образе точки.

LaTeX

$$$(\mathrm{eval}\;f) \circ (\mathrm{toMvPolynomial}\;i) = \mathrm{Polynomial.eval}(f(i))$$$

Lean4

@[simp]
theorem eval_toMvPolynomial (f : σ → R) (i : σ) (p : R[X]) : eval f (p.toMvPolynomial i) = Polynomial.eval (f i) p :=
  DFunLike.congr_fun (eval_comp_toMvPolynomial ..) p

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