le_order — Mathlib

English

If coefficients vanish below ENat n, then n ≤ f.order.

Русский

Если коэффициенты равны нулю для всех д < n, то n ≤ order(f).

LaTeX

$$∀ d, degree d < n → coeff d f = 0 → n ≤ f.order$$

Lean4

/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `degree d < n`. -/
theorem le_order {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, degree d < n → coeff d f = 0) : n ≤ f.order :=
  by
  simp_rw [degree_eq_weight_one] at h
  exact le_weightedOrder _ h

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