powerSeriesPart — Mathlib

English

For a Laurent series x, the associated power series powerSeriesPart(x) is the series with coefficients x.coeff(order(x) + n).

Русский

Для лорантового ряда x связанный степенной ряд powerSeriesPart(x) имеет коэффициенты x.coeff(order(x) + n).

LaTeX

$$$\text{powerSeriesPart}(x) = \sum_{n \ge 0} x_{\mathrm{order}(x)+n} X^{n}$$$

Lean4

/-- This is a power series that can be multiplied by an integer power of `X` to give our
  Laurent series. If the Laurent series is nonzero, `powerSeriesPart` has a nonzero
  constant term. -/
def powerSeriesPart (x : R⸨X⸩) : R⟦X⟧ :=
  PowerSeries.mk fun n => x.coeff (x.order + n)

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