English
There is a natural algebra structure over K on the subring adicCompletionIntegers(RatFunc K)(idealX K), obtained by restricting the canonical map through the Laurent series equivalence.
Русский
Существует естественная структура алгебры над K на подкольце adicCompletionIntegers(RatFunc K)(idealX K), полученная ограничением канонического отображения через эквивалентность Лорантовых рядов.
LaTeX
$$$K \to (\,idealX(K)\).adicCompletionIntegers(\operatorname{RatFunc} K)\text{} \text{ с} a \mapsto ( (\text{LaurentSeriesRingEquiv } K).toRingHom \circ HahnSeries.C)(a) \text{ ограничено}.$$$
Lean4
instance : Algebra K ((idealX K).adicCompletionIntegers (RatFunc K)) :=
RingHom.toAlgebra <|
((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C).codRestrict _ (algebraMap_C_mem_adicCompletionIntegers K)
