eval₂ — Mathlib

English

For any polynomial f ∈ Polynomial R, the power-series evaluation of f considered as a power-series equals its polynomial evaluation.

Русский

Для любого многочлена f ∈ Polynomial R, значение степенного ряда, полученное из f, равно f.eval₂ φ a.

LaTeX

$$$\text{eval}_2 φ\, a\, (f^{\text{toPowerSeries}}) = f.eval_2 φ a$$$

Lean4

/-- Evaluation of a power series `f` at a point `a`.

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 `a` is topologically nilpotent. -/
noncomputable def eval₂ : PowerSeries R → S :=
  MvPowerSeries.eval₂ φ (fun _ ↦ a)

Похожие утверждения