powerSeriesEquivSubring — Mathlib

English

There is a ring isomorphism between PowerSeries K and the subring powerSeries_as_subring K inside LaurentSeries.

Русский

Существует кольцевой изоморфизм между PowerSeries K и подкольцом powerSeries_as_subring K внутри LaurentSeries.

LaTeX

$$$\\mathrm{powerSeriesEquivSubring}\\;K : \\mathrm{PowerSeries}\\,K \\cong \\mathrm{Subtype}\\,\\bigl( x \\in \\mathrm{powerSeries\\_as\\_subring}\\bigr)$$$

Lean4

/-- The ring `K⟦X⟧` is isomorphic to the subring `powerSeries_as_subring K` -/
abbrev powerSeriesEquivSubring : K⟦X⟧ ≃+* powerSeries_as_subring K :=
  ((Subring.topEquiv).symm).trans (Subring.equivMapOfInjective ⊤ (ofPowerSeries ℤ K) ofPowerSeries_injective)

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