intValuation_le_iff_coeff_lt_eq_zero

English

For any D∈ℤ, a Laurent series f satisfies Valued.v f ≤ exp(-D) if and only if all coefficients below D vanish: coeff n f = 0 for n < D.

Русский

Для любого D∈ℤ верна эквивалентность: Valued.v f ≤ exp(-D) тогда и только тогда, когда все коэффициенты ниже D обнуляются: coeff n f = 0 для n < D.

LaTeX

$$$\forall D\in\mathbb{Z},\; Valued.v f \le e^{-D} \iff \forall n\in\mathbb{Z}, n

Lean4

theorem intValuation_le_iff_coeff_lt_eq_zero {d : ℕ} (f : K⟦X⟧) :
    Valued.v (f : K⸨X⸩) ≤ exp (-d : ℤ) ↔ ∀ n : ℕ, n < d → coeff n f = 0 :=
  by
  have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff n) f = 0 :=
    ⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩
  rw [← this, ← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap, ←
    span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow]
  apply intValuation_le_pow_iff_dvd

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