eval₂Hom — Mathlib

English

There is an evaluation homomorphism at a on PowerSeries, as a RingHom, given a continuous φ and HasEval a.

Русский

Существует гомоморфизм оценки в точке a на PowerSeries, как кольцевой гомоморфизм, заданный непрерывным φ и HasEval a.

LaTeX

$$$\text{eval}_2\mathrm{Hom}(h_\phi, h_a) : \text{PowerSeries } R \to^+_* S$$$

Lean4

/-- The evaluation homomorphism at `a` on `PowerSeries`, as a `RingHom`. -/
noncomputable def eval₂Hom (hφ : Continuous φ) (ha : HasEval a) : PowerSeries R →+* S :=
  MvPowerSeries.eval₂Hom hφ (hasEval ha)

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