English
If f is a polynomial, evaluating the associated multivariate power series by eval₂ φ a yields the same result as evaluating the polynomial directly.
Русский
Если f является полиномом, то при подстановке через eval₂ φ a соответствующий многомерный степенной ряд даёт тот же результат, что и прямое вычисление полинома.
LaTeX
$$$$\operatorname{eval}_{\phi}^{a}(f^{\uparrow}) = \operatorname{MvPolynomial.eval}_{\phi}^{a}(f) \quad\text{for } f \in \mathrm{MvPolynomial}(\sigma,R),$$$$
Lean4
@[simp, norm_cast]
theorem eval₂_coe (f : MvPolynomial σ R) : MvPowerSeries.eval₂ φ a f = MvPolynomial.eval₂ φ a f :=
by
have : ∃ p : MvPolynomial σ R, (p : MvPowerSeries σ R) = f := ⟨f, rfl⟩
rw [eval₂, dif_pos this]
congr
rw [← MvPolynomial.coe_inj, this.choose_spec]
