English
The coercion of the algebra-valued evaluation aeval equals eval₂ via the algebra map.
Русский
Приведение к функции алгебраического типа aeval совпадает с eval₂ через алгебраическое отображение.
LaTeX
$$$$\uparrow(\operatorname{aeval}(ha)) = \operatorname{eval}_{\text{algebraMap}(R,S)}^{a}.$$$$
Lean4
/-- Evaluation of power series at adequate elements, as an `AlgHom` -/
noncomputable def aeval (ha : HasEval a) : MvPowerSeries σ R →ₐ[R] S
where
toRingHom := MvPowerSeries.eval₂Hom (continuous_algebraMap R S) ha
commutes'
r := by
simp only [toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe]
rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]