English
Substituting a into a power series f is defined by substitution as an evaluation: subst a f := eval₂ (algebraMap R S) a f.
Русский
Подстановка a в степенной ряд f определяется как подстановочное вычисление: subst a f := eval₂ (algebraMap R S) a f.
LaTeX
$$$\\operatorname{subst}(a,f) = \\operatorname{eval}_2(\\operatorname{algebraMap} R S)\\ a\\ f$$$
Lean4
/-- Substitution of power series into a power series
It coincides with evaluation when `f` is a polynomial, or under `HasSubst a`.
Otherwise, it is given the dummy value `0`. -/
noncomputable def subst (a : σ → MvPowerSeries τ S) (f : MvPowerSeries σ R) : MvPowerSeries τ S :=
letI : UniformSpace R := ⊥
letI : UniformSpace S := ⊥
eval₂ (algebraMap _ _) a f
