instAlgebraRatFuncAdicCompl — Mathlib

English

There is a natural K-algebra structure on RatFuncAdicCompl K induced by composing the Laurent-series isomorphism with HahnSeries constants.

Русский

Существует естественная структура K-алгебры на RatFuncAdicCompl K, получаемая композицией изоморфизма Лорентсовых рядов с константами HahnSeries.

LaTeX

$$$\\text{Algebra }K\\; (\\mathrm{RatFuncAdicCompl}\\,K) = \\mathrm{RingHom}.toAlgebra\\left( (\\mathrm{LaurentSeriesRingEquiv}\\,K) .\\mathrm{toRingHom} \\circ \\mathrm{HahnSeries.C} \\right)$$$

Lean4

instance : Algebra K (RatFuncAdicCompl K) :=
  RingHom.toAlgebra ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C)

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