English
The uniform space isomorphism between RatFuncAdicCompl K and K⟨X⟩ is the inverse of the fundamental one; it provides a symmetric uniform identification of the two completions.
Русский
Униформное изоморфизм между RatFuncAdicCompl K и K⟨X⟩ является обратным по отношению к базовому изоморфизму, обеспечивая симметрическую идентификацию завершений.
LaTeX
$$$\\text{ratfuncAdicComplRingEquiv}\\,K \\;\\text{is inverse to the fundamental one}$$$
Lean4
/-- The uniform space equivalence between two abstract completions of `ratfunc K` as a ring
equivalence: this will be the *inverse* of the fundamental one. -/
abbrev ratfuncAdicComplRingEquiv : RatFuncAdicCompl K ≃+* K⸨X⸩ :=
{
comparePkg K with
map_mul' := by
intro x y
rw [comparePkg_eq_extension, (extensionAsRingHom K (continuous_coe)).map_mul']
rfl
map_add' := by
intro x y
rw [comparePkg_eq_extension, (extensionAsRingHom K (continuous_coe)).map_add']
rfl }
