powerSeriesEquivSubring_coe_apply

English

The component of powerSeriesEquivSubring on a power series f matches the coe from HahnSeries to PowerSeries.

Русский

Компонента powerSeriesEquivSubring на ряд мощности f совпадает с вложением через HahnSeries.

LaTeX

$$$\\bigl(p\\_\\mathrm{owerSeriesEquivSubring}(K)\\bigr)(f) = \\operatorname{ofPowerSeries}_{\\mathbb{Z},K}(f)$$$

Lean4

theorem powerSeriesEquivSubring_coe_apply (f : K⟦X⟧) : (powerSeriesEquivSubring K f : K⸨X⸩) = ofPowerSeries ℤ K f :=
  rfl

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