English
If x belongs to the integers inside the adic completion, then there exists a power series F with LaurentSeriesRingEquiv K mapping to x.
Русский
Если x принадлежит целым внутри адикционного завершения, тогда существует ряд мощности F, отображаемый через LaurentSeriesRingEquiv на x.
LaTeX
$$$\\exists F:\\,K\\langle\\!X\\!\\rangle,\\; (\\mathrm{LaurentSeriesRingEquiv}\\;K)\\;F = x$$$
Lean4
theorem exists_powerSeries_of_memIntegers {x : RatFuncAdicCompl K}
(hx : x ∈ (idealX K).adicCompletionIntegers (RatFunc K)) : ∃ F : K⟦X⟧, (LaurentSeriesRingEquiv K) F = x :=
by
set f := (ratfuncAdicComplRingEquiv K) x with hf
have H_x : (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((ratfuncAdicComplRingEquiv K) x) = x :=
congr_fun (inverse_compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) x
rw [mem_adicCompletionIntegers, ← H_x] at hx
obtain ⟨F, hF⟩ := (val_le_one_iff_eq_coe K f).mp (valuation_compare _ f ▸ hx)
exact ⟨F, by rw [hF, hf, RingEquiv.symm_apply_apply]⟩
