coeff_zero_of_lt_intValuation — Mathlib

English

If a Laurent series f has valuation ≤ exp(-d) for some natural d, then all coefficients up to index d−1 vanish: coeff n f = 0 for n < d.

Русский

Если лорантов ряд f имеет валюацию ≤ exp(-d), тогда все коэффициенты с индексами меньше d нуля: coeff n f = 0 для n < d.

LaTeX

$$$H: \text{Valued.v}(f) \le e^{-d},\; n

Lean4

theorem coeff_zero_of_lt_intValuation {n d : ℕ} {f : K⟦X⟧} (H : Valued.v (f : K⸨X⸩) ≤ exp (-d : ℤ)) :
    n < d → coeff n f = 0 := by
  intro hnd
  apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
  rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap, exp,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX, Ideal.span_singleton_pow,
    span_singleton_dvd_span_singleton_iff_dvd] at H

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