eq_coeff_of_valuation_sub_lt — Mathlib

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

Похожие утверждения