eval₂Hom_eq_extend — Mathlib

English

The evaluation homomorphism equals the extension of polynomial evaluation along the dense embedding.

Русский

Гомоморфизм оценивания равен продолжению полиномиальной оценки вдоль плотного внедрения.

LaTeX

$$$$\operatorname{eval₂Hom}(h\phi,ha) = \text{toMvPowerSeries_isDenseInducing}.extend (\operatorname{MvPolynomial.eval}_{\phi}^{a}) f,$$$$

Lean4

theorem eval₂Hom_eq_extend (hφ : Continuous φ) (ha : HasEval a) (f : MvPowerSeries σ R) :
    eval₂Hom hφ ha f = toMvPowerSeries_isDenseInducing.extend (MvPolynomial.eval₂ φ a) f :=
  rfl

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