English
If ε is a continuous ring hom whose restriction to polynomials matches eval₂ φ a, then ε = eval₂ φ a on all power series.
Русский
Если ε — непрерывный гомоморфизм колец, совпадающий с eval₂ φ a на полиномах, то он совпадает и на всех степенных рядах.
LaTeX
$$$$\forall {\varepsilon : \mathrm{MvPowerSeries}(\sigma,R) \to S},\; \text{Continuous}(\varepsilon) \wedge (\forall p, \varepsilon(p^{\uparrow}) = \operatorname{MvPolynomial.eval}_{\phi}^{a}(p)) \Rightarrow \varepsilon = \operatorname{eval}_{\phi}^{a}.$$$$
Lean4
theorem eval₂_unique (hφ : Continuous φ) (ha : HasEval a) {ε : MvPowerSeries σ R → S} (hε : Continuous ε)
(h : ∀ p : MvPolynomial σ R, ε p = MvPolynomial.eval₂ φ a p) : ε = eval₂ φ a :=
by
rw [← coe_eval₂Hom hφ ha]
exact (toMvPowerSeries_isDenseInducing.extend_unique h hε).symm
