English
The coefficient formula for substituted powers: coeff_e (subst a f) equals the finitely supported sum of coeff_d f times coeff_e (a^d).
Русский
Формула коэффициентов для подстановки: коэффициент e подстановки равен конечной сумме coeff_d f · coeff_e (a^d).
LaTeX
$$$\\forall ha\\, (f : PowerSeries R)\\, (e : Finsupp\\tau \\mathbb{N}),\n \\big(\\mathrm{coeff}\,e\\big)(\\mathrm{subst} a f) = \\sum_d coeff_d f · coeff_e (a^d)$$$
Lean4
theorem coeff_subst (ha : HasSubst a) (f : PowerSeries R) (e : τ →₀ ℕ) :
MvPowerSeries.coeff e (subst a f) = finsum (fun (d : ℕ) ↦ coeff d f • (MvPowerSeries.coeff e (a ^ d))) :=
by
rw [subst, MvPowerSeries.coeff_subst ha.const f e, ←
finsum_comp_equiv (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm]
apply finsum_congr
intro
congr <;> simp
