English
There is a canonical K-algebra isomorphism between the Laurent series ring K⟦X⟧ and the X-adic completion integers of RatFunc K.
Русский
Существует каноническое K-алгебраическое изоморфизм между кольцом Лорантовых рядов K⟦X⟧ и X-адической завершённостью RatFunc K.
LaTeX
$$$K\lbrace\!X\rbrace\!\_K \cong_K (\operatorname{idealX} K)\operatorname{adicCompletionIntegers}(\operatorname{RatFunc} K).$$$
Lean4
/-- The algebra isomorphism between `K⟦X⟧` and the unit ball inside the `X`-adic completion of
`RatFunc K`. -/
def powerSeriesAlgEquiv : K⟦X⟧ ≃ₐ[K] (idealX K).adicCompletionIntegers (RatFunc K) :=
by
apply AlgEquiv.ofRingEquiv (f := powerSeriesRingEquiv K)
intro a
rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj, powerSeriesRingEquiv_coe_apply,
RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)]
simp
