English
There exists a canonical ring homomorphism from the X-adic completion of RatFunc K to LaurentSeries K, obtained by extending the natural algebra map RatFunc K → LaurentSeries K to the completion.
Русский
Существуют каноническое кольцо-гомоморфизм от X-адического дополнения RatFunc K к LaurentSeries K, полученный продлением естественного алгебраического отображения RatFunc K → LaurentSeries K до дополнения.
LaTeX
$$$\mathrm{extensionAsRingHom} = \mathrm{UniformSpace.Completion.extensionHom}(\mathrm{algebraMap}(\mathrm{RatFunc}\,K) \; (\mathrm{LaurentSeries}\,K))$$$
Lean4
/-- Reinterpret the extension of `coe : RatFunc K → K⸨X⸩` as a ring homomorphism -/
abbrev extensionAsRingHom :=
UniformSpace.Completion.extensionHom (algebraMap (RatFunc K) (K⸨X⸩))
