English
The coefficient of a substituted power series is given by a finite sum over d of coeff d f times coeff e (a^d).
Русский
Коэффициент подстановки равен сумме по d коэффициента d f, умноженного на коэффициент e (a^d).
LaTeX
$$$\forall ha\, (f : PowerSeries R)\, (e : Finsupp\tau \mathbb{N}),\
\text{coeff e in }(subst a f) = \sum_d coeff_d f \cdot coeff_e (a^d)$$$
Lean4
theorem coeff_subst_finite (ha : HasSubst a) (f : PowerSeries R) (e : τ →₀ ℕ) :
Set.Finite (fun (d : ℕ) ↦ coeff d f • MvPowerSeries.coeff e (a ^ d)).support :=
by
convert (MvPowerSeries.coeff_subst_finite ha.const f e).image (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv
rw [← Equiv.preimage_eq_iff_eq_image, ← Function.support_comp_eq_preimage]
apply congr_arg
rw [← Equiv.eq_comp_symm]
ext
simp [coeff]
