English
For any s : Fin n → R, y ∈ R, and f ∈ MvPolynomial(Fin(n+1)) R, the equation holds equating eval with an eval_map composition through finSuccEquiv.
Русский
Для любых s, y и f верно равенство, связывающее eval и композицию через finSuccEquiv.
LaTeX
$$$\\operatorname{eval} (\\operatorname{Fin.cons} y\, s)\\; f = \\operatorname{Polynomial}.eval\\; y\\bigl(\\operatorname{Polynomial}.map(\\operatorname{eval} s) (\\operatorname{finSuccEquiv} R n\\; f)\\bigr)$$$
Lean4
theorem eval_eq_eval_mv_eval' (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
eval (Fin.cons y s : Fin (n + 1) → R) f = Polynomial.eval y (Polynomial.map (eval s) (finSuccEquiv R n f)) := by
-- turn this into a def `Polynomial.mapAlgHom`
let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
{ Polynomial.mapRingHom (eval s) with
commutes' := fun r => by
convert Polynomial.map_C (eval s)
exact (eval_C _).symm }
change aeval (Fin.cons y s : Fin (n + 1) → R) f = (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
congr 2
apply MvPolynomial.algHom_ext
rw [Fin.forall_iff_succ]
simp only [φ, aeval_X, Fin.cons_zero, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
Polynomial.map_C, AlgHom.coe_mk, Polynomial.coe_mapRingHom, comp_apply, finSuccEquiv_apply, eval₂Hom_X',
Fin.cases_zero, Polynomial.map_X, Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, eval_X, Polynomial.eval_C,
AlgHom.coe_coe, implies_true, and_self]
