aeval_unique — Mathlib

English

If ha is HasEval a, then for p ∈ MvPolynomial σ R we have aeval ha (p : MvPowerSeries σ R) = p.aeval a.

Русский

Если ha имеет отображение a, то для p ∈ MvPolynomial σ R выполняется aeval ha (p : MvPowerSeries σ R) = p.aeval a.

LaTeX

$$$ \mathrm{aeval}_{ha}(p : \MvPowerSeries_{\sigma} R) = p\,.\mathrm{aeval}(a) $$$

Lean4

theorem aeval_unique {ε : MvPowerSeries σ R →ₐ[R] S} (hε : Continuous ε) : aeval (HasEval.X.map hε) = ε :=
  by
  apply DFunLike.ext'
  rw [coe_aeval]
  refine (eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm
  intro p
  trans ε.comp (coeToMvPowerSeries.algHom R) p
  · simp
  conv_lhs => rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]
  simp

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