English
Let x be an element of K. The image ((LaurentSeriesRingEquiv K).toRingHom ∘ HahnSeries.C)(x) lies in the X-adic completion integers of RatFunc K, i.e. in adicCompletionIntegers(RatFunc K, idealX K).
Русский
Пусть a ∈ K. Образ ((LaurentSeriesRingEquiv K).toRingHom ∘ HahnSeries.C)(a) принадлежит адик-комплиту целочисленного RatFunc K по идеалу X, то есть принадлежит adicCompletionIntegers(RatFunc K, idealX K).
LaTeX
$$$\big( (\text{LaurentSeriesRingEquiv } K).toRingHom \circ HahnSeries.C \big)(x) \in \operatorname{adicCompletionIntegers}(\operatorname{RatFunc} K, \mathfrak{X} K).$$$
Lean4
theorem algebraMap_C_mem_adicCompletionIntegers (x : K) :
((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ adicCompletionIntegers (RatFunc K) (idealX K) :=
by
have : HahnSeries.C x = ofPowerSeries ℤ K (PowerSeries.C x) := by simp [C_apply, ofPowerSeries_C]
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, this]
apply LaurentSeriesRingEquiv_mem_valuationSubring
