substAlgHom_coe — Mathlib

English

If a substitution ha is given, then for any polynomial p, substAlgHom ha applied to p (viewed as a power series) equals the evaluation of p at a via a.

Русский

Если дано подстановочное отображение ha, то для любого полинома p, применение substAlgHom ha к p (рассматриваемому как степенной ряд) равно вычислению p на a через a.

LaTeX

$$$\\operatorname{substAlgHom}(ha)(p) = \\bigl(\\operatorname{aeval} a\\, p\\bigr)$$$

Lean4

theorem substAlgHom_coe (ha : HasSubst a) (p : Polynomial R) :
    substAlgHom ha (p : PowerSeries R) = ↑(Polynomial.aeval a p) :=
  by
  rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom, MvPowerSeries.subst_coe, ←
    AlgHom.comp_apply]
  apply AlgHom.congr_fun
  apply Polynomial.algHom_ext
  simp

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