English
For RatFunc K, the valuation computed in polynomial terms matches the valuation computed after embedding RatFunc into LaurentSeries and evaluating with the PowerSeries ideal.
Русский
Для RatFunc K валюация, вычисленная через полиномы, совпадает с валюацией после вложения RatFunc в LaurentSeries и вычисления через PowerSeries.
LaTeX
$$$\text{valuation}_{{\text{RatFunc} }}(P) = \text{valuation}_{\text{PowerSeries}}(P)$.$$
Lean4
theorem valuation_eq_LaurentSeries_valuation (P : RatFunc K) :
(Polynomial.idealX K).valuation _ P = (PowerSeries.idealX K).valuation K⸨X⸩ P :=
by
refine RatFunc.induction_on' P ?_
intro f g h
rw [Polynomial.valuation_of_mk K f h, RatFunc.mk_eq_mk' f h, Eq.comm]
convert
@valuation_of_mk' K⟦X⟧ _ _ K⸨X⸩ _ _ _ (PowerSeries.idealX K) f
⟨g, mem_nonZeroDivisors_iff_ne_zero.2 <| (by simp [h])⟩
· simp [← IsScalarTower.algebraMap_apply K[X] (RatFunc K) K⸨X⸩]
exacts [intValuation_eq_of_coe _, intValuation_eq_of_coe _]
