English
Let φ: R →+* S be a ring homomorphism and a : σ → S a point in S for each index. The evaluation map on a multivariate power series is defined so that it agrees with evaluating f as a polynomial when f comes from a polynomial, and otherwise is obtained by a continuous/dense extension of this polynomial evaluation to the full space of multivariate power series.
Русский
Пусть φ: R →+* S — гомоморфизм колец и пусть a: σ → S задаёт значения переменных. Оценивание многопеременного степенного ряда задаётся так, что оно совпадает с оценкой полинома, если степенной ряд является подобием полинома, иначе оценивание получено как непрерывное/плотное продолжение полевой оценки до всего пространства многопеременных степенных рядов.
LaTeX
$$$$\\operatorname{eval}_{\\phi}^{a}(f) = \\begin{cases} \\operatorname{MvPolynomial.eval}_{\\phi}^{a}(p), & \\text{if } f = p \\text{ for some } p \\in \\mathrm{MvPolynomial}(\\sigma,R), \\\\ \\text{IsDenseInducing.extend}(\\operatorname{MvPolynomial.eval}_{\\phi}^{a}, f), & \\text{otherwise}. \\end{cases}$$$$
Lean4
/-- Evaluation of a multivariate power series at `f` at a point `a : σ → S`.
It coincides with the evaluation of `f` as a polynomial if `f` is the coercion of a polynomial.
Otherwise, it is only relevant if `φ` is continuous and `HasEval a`. -/
noncomputable def eval₂ (f : MvPowerSeries σ R) : S :=
if H : ∃ p : MvPolynomial σ R, p = f then (MvPolynomial.eval₂ φ a H.choose)
else IsDenseInducing.extend toMvPowerSeries_isDenseInducing (MvPolynomial.eval₂ φ a) f
