English
Let x be a Hahn series with coefficients in R indexed by Γ and f a power series over R. For every g ∈ Γ, the g-th coefficient of the element heval x f is the finite sum of the g-th coefficients of the power series family (powerSeriesFamily x f).
Русский
Пусть x — ряд Хана с коэффициентами в R, индексированными по Γ, и f — степенной ряд над R. Для каждого g ∈ Γ коэффициент при g у элемента heval x f равен конечной сумме коэффициентов ряда степеней family (powerSeriesFamily x f) при g.
LaTeX
$$$ (\\text{heval } x\, f).\\mathrm{coeff}\; g = \\sum^{\\mathrm{fin}}_{n} ((\\text{powerSeriesFamily } x\, f).\\mathrm{coeff}\; g)\\, n $$$
Lean4
theorem coeff_heval (f : PowerSeries R) (g : Γ) : (heval x f).coeff g = ∑ᶠ n, ((powerSeriesFamily x f).coeff g) n :=
by
rw [heval_apply, coeff_hsum]
exact rfl
