eval₂_unique — Mathlib

English

If two evaluation maps agree on polynomials, they agree on all power series.

Русский

Если две оценки совпадают на полиномах, совпадают на всех степенных рядах.

LaTeX

$$$\text{Continuous } φ \rightarrow \text{HasEval } a \rightarrow \forall f, \text{HasSum } ? \Rightarrow \text{eq eval₂ φ a f}$$$

Lean4

theorem eval₂_unique (hφ : Continuous φ) (ha : HasEval a) {ε : PowerSeries R → S} (hε : Continuous ε)
    (h : ∀ p : Polynomial R, ε p = Polynomial.eval₂ φ a p) : ε = eval₂ φ a :=
  by
  apply MvPowerSeries.eval₂_unique hφ (hasEval ha) hε
  intro p
  rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_pUnitAlgEquiv]

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