English
The comparison map between completions preserves the valuation: applying Valued.v after the compare map yields the same as evaluating Valued.v directly on f.
Русский
Сопоставляющее отображение между завершениями сохраняет ценность: применение Valued.v после compare возвращает ту же величину, что и прямое вычисление ценности на f.
LaTeX
$$$\\mathrm{Valued.v} \\bigl(\\mathrm{AbstractCompletion.compare}\\bigl(\\mathrm{LaurentSeriesPkg}\\,K\\bigr)\\; f\\bigr) = \\mathrm{Valued.v}(f)$$$
Lean4
theorem valuation_compare (f : K⸨X⸩) :
(Valued.v : (RatFuncAdicCompl K) → ℤᵐ⁰) (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) =
Valued.v f :=
by
rw [← valuation_LaurentSeries_equal_extension, ←
compare_comp_eq_compare (pkg := ratfuncAdicComplPkg) (cont_f := Valued.continuous_valuation)]
· rfl
exact (tendsto_valuation K)
