toPowerSeries — Mathlib

English

There is a natural inclusion from polynomials into formal power series, sending a polynomial to the power series whose nth coefficient is the nth coefficient of the polynomial.

Русский

Существует естественное включение полиномов в формальные степенные ряды, отправляющее полином в степенной ряд, чьи n-ый коэффициент совпадает с коэффициентом полинома.

LaTeX

$$$\\operatorname{toPowerSeries}(\\varphi) = \\operatorname{PowerSeries.mk}(\\lambda n.\\ \\operatorname{coeff}(\\varphi,n))$$$

Lean4

/-- The natural inclusion from polynomials into formal power series. -/
@[coe]
def toPowerSeries : R[X] → PowerSeries R := fun φ => PowerSeries.mk fun n => coeff φ n

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