English
Let d and n be integers, and f,g be Laurent series over K. If the valuation v(g − f) ≤ exp(−d), then for every n < d we have g.coeff n = f.coeff n.
Русский
Пусть d и n целые числа, а f,g — лаурентовые серии над K. Если валюация v(g − f) ≤ e^(−d), то для каждого n < d выполняется g_n = f_n.
LaTeX
$$$\forall d,n \in \mathbb{Z},\ f,g \in K⸨X⸩,\ \mathrm{v}(g-f) \le e^{-d} \implies n < d \implies g.\mathrm{coeff}(n) = f.\mathrm{coeff}(n).$$$
Lean4
theorem eq_coeff_of_valuation_sub_lt {d n : ℤ} {f g : K⸨X⸩} (H : Valued.v (g - f) ≤ exp (-d)) :
n < d → g.coeff n = f.coeff n := by
by_cases triv : g = f
· exact fun _ => by rw [triv]
· intro hn
apply eq_of_sub_eq_zero
rw [← HahnSeries.coeff_sub]
apply coeff_zero_of_lt_valuation K H hn