English
Substitution respects multiplication: substituting into a product equals the product of substitutions.
Русский
Подстановка сохраняет произведение: подстановка в произведение равна произведению подстановок.
LaTeX
$$$\forall ha\,\forall f,g:\ PowerSeries\,R,\ subst a (f\cdot g) = subst a f \cdot subst a g$$$
Lean4
/-- Rewrite `PowerSeries.substAlgHom` as `PowerSeries.aeval`.
Its use is discouraged because it introduces a topology and might lead
into awkward comparisons. -/
theorem substAlgHom_eq_aeval [UniformSpace R] [DiscreteUniformity R] [UniformSpace S] [DiscreteUniformity S]
(ha : HasSubst a) : (substAlgHom ha : R⟦X⟧ →ₐ[R] MvPowerSeries τ S) = PowerSeries.aeval ha.hasEval :=
by
ext1 f
simpa [substAlgHom] using congr_fun (MvPowerSeries.substAlgHom_eq_aeval ha.const) f
