aeval — Mathlib

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]

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