coeToPowerSeries — Mathlib

English

There is a canonical coercion from polynomials to power series given by the inclusion toPowerSeries.

Русский

Существует каноническое включение полиномов в формальные степенные ряды посредством toPowerSeries.

LaTeX

$$$\\text{There is a canonical coercion } (\\uparrow): R[X]\\to PowerSeries R \\text{ given by } toPowerSeries$$$

Lean4

/-- The natural inclusion from polynomials into formal power series. -/
instance coeToPowerSeries : Coe R[X] (PowerSeries R) :=
  ⟨toPowerSeries⟩

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