ratfuncAdicComplPkg — Mathlib

English

The X-adic completion of RatFunc(K) is realized by LaurentSeries(K) as an abstract completion.

Русский

X-адическое дополнение RatFunc(K) реализуется через LaurentSeries(K) как абстрактное дополнение.

LaTeX

$$$\mathrm{ratfuncAdicComplPkg} : \mathsf{AbstractCompletion}(\mathrm{RatFunc}(K)) \text{ with space } K\langle X\rangle \text{ and inclusion map}.$$$

Lean4

/-- The `X`-adic completion as an abstract completion of `RatFunc K` -/
abbrev ratfuncAdicComplPkg : AbstractCompletion (RatFunc K) :=
  UniformSpace.Completion.cPkg

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