LaurentSeriesAlgEquiv — Mathlib

English

There is an algebra equivalence between K⸨X⸩ and RatFuncAdicCompl K, built from a ring isomorphism.

Русский

Существует алгебра-эквивалентность между K⸨X⸩ и RatFuncAdicCompl K, построенная из кольцевого изоморфизма.

LaTeX

$$$\\text{LaurentSeriesAlgEquiv}\\;K : K⌀X⌀ \\cong_K\\; \\mathrm{RatFuncAdicCompl}\\,K$$$

Lean4

/-- The algebra equivalence between `K⸨X⸩` and the `X`-adic completion of `RatFunc X` -/
def LaurentSeriesAlgEquiv : K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K :=
  AlgEquiv.ofRingEquiv (f := LaurentSeriesRingEquiv K) (fun a ↦ by simp [RingHom.algebraMap_toAlgebra])

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