LaurentSeriesRingEquiv — Mathlib

English

There is a ring isomorphism between LaurentSeries K and RatFuncAdicCompl K.

Русский

Существует кольцевой изоморфизм между кольцом Лорентских рядов и RatFuncAdicCompl K.

LaTeX

$$$\\operatorname{LaurentSeries} K \\cong \\operatorname{LaurentSeries.RatFuncAdicCompl} K$$$

Lean4

/-- The uniform space equivalence between two abstract completions of `ratfunc K` as a ring
equivalence: it goes from `K⸨X⸩` to `RatFuncAdicCompl K` -/
abbrev LaurentSeriesRingEquiv : K⸨X⸩ ≃+* RatFuncAdicCompl K :=
  (ratfuncAdicComplRingEquiv K).symm

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