coeff_toPowerSeries_symm — Mathlib

English

The nth coefficient of the power-series-to-Hahn-series translation equals the nth coefficient of the original power series.

Русский

Каждый коэффициент n перехода от степенного ряда к Hahn-преобразованию равен соответствующему коэффициенту n исходного степенного ряда.

LaTeX

$$$ \mathrm{PowerSeries.coeff\} n (\mathrm{toPowerSeries}\ f) = \mathrm{HahnSeries.coeff}\ n \, f $$$

Lean4

theorem coeff_toPowerSeries_symm {f : PowerSeries R} {n : ℕ} :
    (HahnSeries.toPowerSeries.symm f).coeff n = PowerSeries.coeff n f :=
  rfl

Похожие утверждения