English
The constant term of the substituted series is the finite sum of the products of coefficients of f with the constant coefficients of the substituted monomials.
Русский
Постоянный коэффициент подстановки равен конечной сумме произведений коэффициентов f и констант подстановок мономиалов.
LaTeX
$$$\\operatorname{constantCoeff}(\\operatorname{subst}(a,f)) = \\operatorname{finsum}( d \\mapsto \\operatorname{coeff}_{d} f \\cdot \\operatorname{constantCoeff}(d.\\prod (a_s)^e) )$$$
Lean4
theorem constantCoeff_subst (ha : HasSubst a) (f : MvPowerSeries σ R) :
constantCoeff (subst a f) = finsum (fun d ↦ coeff d f • (constantCoeff (d.prod fun s e => (a s) ^ e))) := by
simp only [← coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]