comparePkg — Mathlib

English

There is a uniform space isomorphism between RatFuncAdicCompl K and the Laurent series ring K⎨X⎩, i.e. they are uniformly equivalent completions.

Русский

Существует униформное изоморфизм между RatFuncAdicCompl K и кольцом Лорентских рядов K⎨X⎩, то есть обе аппроксимации совместимы по равномерной структуре.

LaTeX

$$$\\operatorname{RatFuncAdicCompl} K \\;\\simeq_{\\mathcal{U}}\\; K\\langle X\\rangle$$$

Lean4

/-- The uniform space isomorphism between two abstract completions of `ratfunc K` -/
abbrev comparePkg : RatFuncAdicCompl K ≃ᵤ K⸨X⸩ :=
  compareEquiv ratfuncAdicComplPkg (LaurentSeriesPkg K)

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