English
LaurentSeriesPkg is the abstract completion of RatFunc(K) with space K⟨X⟩ and coe given by inclusion.
Русский
LaurentSeriesPkg является абстрактным дополнением RatFunc(K) с пространством K⟨X⟩ и отображением включения.
LaTeX
$$$\mathrm{LaurentSeriesPkg}(K) : \mathsf{AbstractCompletion}(\mathrm{RatFunc}(K)) \text{ with space } K\langle X\rangle \text{ and } \mathrm{coe}=\uparrow.$$$
Lean4
/-- Having established that the `K⸨X⸩` is complete and contains `RatFunc K` as a dense
subspace, it gives rise to an abstract completion of `RatFunc K`. -/
noncomputable def LaurentSeriesPkg : AbstractCompletion (RatFunc K)
where
space := K⸨X⸩
coe := (↑)
uniformStruct := inferInstance
complete := inferInstance
separation := inferInstance
isUniformInducing := inducing_coe
dense := coe_range_dense
