eval₂Hom — Mathlib

English

There is a ring hom from multivariate power series to S extending evaluation at φ and a, under suitable topological hypotheses.

Русский

Существуют гомоморфизм колец из многовекторного ряда в S, расширяющий оценку через φ и a при подходящих топологических предпосылках.

LaTeX

$$$$\text{eval₂Hom}_{h\phi,ha} : \mathrm{MvPowerSeries}(\sigma,R) \to R\; S,$$$$

Lean4

/-- Evaluation of power series at adequate elements, as a `RingHom` -/
noncomputable def eval₂Hom (hφ : Continuous φ) (ha : HasEval a) : MvPowerSeries σ R →+* S :=
  IsDenseInducing.extendRingHom (i := coeToMvPowerSeries.ringHom) toMvPowerSeries_isUniformInducing
    denseRange_toMvPowerSeries (toMvPowerSeries_uniformContinuous hφ ha)

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