English
Let ha be HasEval a and ε : S →ₐ[R] T be a continuous algebra hom. Then the composition ε ∘ (aeval ha) equals aeval (ha.map hε); i.e., ε ∘ aeval ha = aeval (ha.map hε).
Русский
Пусть ha = HasEval a и ε : S →ₐ[R] T непрерывное алгебраическое гомоморфирование. Тогда композиция ε ∘ aeval ha равна aeval (ha.map hε); то есть ε ∘ aeval ha = aeval (ha.map hε).
LaTeX
$$$ \varepsilon \circ (\mathrm{aeval}\ ha) = \mathrm{aeval}\ (ha.map\ h\varepsilon) $$$
Lean4
theorem comp_aeval (ha : HasEval a) {T : Type*} [CommRing T] [UniformSpace T] [IsUniformAddGroup T]
[IsTopologicalRing T] [IsLinearTopology T T] [T2Space T] [Algebra R T] [ContinuousSMul R T] [CompleteSpace T]
{ε : S →ₐ[R] T} (hε : Continuous ε) : ε.comp (aeval ha) = aeval (ha.map hε) :=
MvPowerSeries.comp_aeval (hasEval ha) hε
