English
Let b be a substitution of a multivariate power series over R, and f be a power series in R⟦X⟧. For every nonnegative integer e, the e-th coefficient of the substituted series f.subst b equals the finite sum over all d ≥ 0 of the d-th coefficient of f multiplied by the e-th coefficient of b^d.
Русский
Пусть b задаёт подстановку многопеременного степенного ряда над R, а f — степенный ряд в R⟦X⟧. Тогда для каждого неотрицательного числа e коэффициент e подстановки f(b) равен конечной сумме по d ≥ 0: коэффициент d от f, умноженный на коэффициент e от b^d.
LaTeX
$$$\\operatorname{coeff}_e\\bigl(f\\circ b\\bigr) = \\sum_{d \\ge 0} \\operatorname{coeff}_d f \\cdot \\operatorname{coeff}_e\\bigl(b^d\\bigr)$$$
Lean4
theorem coeff_subst' {b : S⟦X⟧} (hb : HasSubst b) (f : R⟦X⟧) (e : ℕ) :
coeff e (f.subst b) = finsum (fun (d : ℕ) ↦ coeff d f • PowerSeries.coeff e (b ^ d)) := by
simp [PowerSeries.coeff, coeff_subst hb]
