coeff_coe_powerSeries — Mathlib

English

If x is a Laurent series coming from a power series, then its nth coefficient (as a Laurent series) equals the nth coefficient of x viewed as a power series.

Русский

Если x — Лаурентовый ряд, полученный из степенного ряда, то его n-й коэффициент совпадает с коэффициентом степенного ряда, от которого получен x.

LaTeX

$$$\operatorname{coeff}_{\text{HahnSeries}}(x,n) = \operatorname{PowerSeries.coeff}(n)\, x$$$

Lean4

@[simp]
theorem coeff_coe_powerSeries (x : R⟦X⟧) (n : ℕ) : HahnSeries.coeff (x : R⸨X⸩) n = PowerSeries.coeff n x := by
  rw [ofPowerSeries_apply_coeff]

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