English
Let ha be a substitution a and hb a HasEval b. For any f, evaluating the substituted series with algebra maps S→T and R→T via eval₂ is the same as first evaluating the inner substitution and then evaluating with R→T.
Русский
Пусть ha — подстановка a, hb — HasEval b. Для любой f вычисления подчленой серии с алгебраическими отображениями S→T и R→T по eval₂ эквивалентны последовательным вычислениям внутренней подстановки и затем eval₂.
LaTeX
$$$\operatorname{eval}_2(\mathrm{algebraMap}\, S\, T, b, \operatorname{subst}_a f) = \operatorname{eval}_2(\mathrm{algebraMap}\, R\, T, \lambda s. \operatorname{eval}_2(\mathrm{algebraMap}\, S\, T, b, a(s)), f)$$$
Lean4
theorem eval₂_subst [UniformSpace R] [DiscreteUniformity R] [UniformSpace S] [DiscreteUniformity S] (ha : HasSubst a)
{b : τ → T} (hb : HasEval b) (f : MvPowerSeries σ R) :
eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f :=
by
let ε : MvPowerSeries τ S →ₐ[R] T := (aeval hb).restrictScalars R
have hε : Continuous ε := continuous_aeval hb
simpa only [AlgHom.coe_restrictScalars', AlgHom.toRingHom_eq_coe, AlgHom.coe_restrictScalars, RingHom.coe_coe, ε,
coe_aeval] using comp_subst_apply ha hε f
