English
For any polynomial p over R, the canonical embedding of p into ordinary power series equals the multivariate-power-series interpretation of aeval at X applied to p.
Русский
Для любого полинома p над R тождественно выполняется, что его каноническое вложение в обычный степенной ряд совпадает с интерпретацией p через MV-полиномы после применения aeval к X.
LaTeX
$$$p^{\\toPowerSeries} = \\bigl((p^{aeval}(\\mathsf{X}())\\, p) : \\mathrm{MvPowerSeries Unit R}\\bigr)$$$
Lean4
theorem _root_.Polynomial.toPowerSeries_toMvPowerSeries (p : Polynomial R) :
(p : PowerSeries R) = ((Polynomial.aeval (MvPolynomial.X ()) p : MvPolynomial Unit R) : MvPowerSeries Unit R) :=
by
suffices
(Polynomial.coeToPowerSeries.algHom R) p =
(MvPolynomial.coeToMvPowerSeries.algHom R) (Polynomial.aeval (MvPolynomial.X () : MvPolynomial Unit R) p)
by simpa
rw [← AlgHom.comp_apply]
apply AlgHom.congr_fun
apply Polynomial.algHom_ext
simp [X]
