powerSeries_as_subring — Mathlib

English

The alias powerSeries_as_subring of K⎯⎧X⎫ is viewed as a subring of K⸨X⸩, via HahnSeries.

Русский

Алиас powerSeries_as_subring K⎯⎧X⎫ считается подкольцом K⸨X⸩ через HahnSeries.

LaTeX

$$$\\text{powerSeries\\_as\\_subring}\\;K \\subseteq \\text{LaurentSeries}$$$

Lean4

/-- In order to compare `K⟦X⟧` with the valuation subring in the `X`-adic completion of
`RatFunc K` we consider its alias as a subring of `K⸨X⸩`. -/
abbrev powerSeries_as_subring : Subring K⸨X⸩ :=
  Subring.map (HahnSeries.ofPowerSeries ℤ K) ⊤

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