order_le — Mathlib

English

If some coefficient is nonzero, then the order is less than or equal to the degree of that coefficient.

Русский

Если некоторый коэффициент ненулевой, тогда порядок не превосходит степень этого коэффициента.

LaTeX

$$coeff d f ≠ 0 → f.order ≤ degree d$$

Lean4

/-- If the `d`th coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to `degree d`. -/
theorem order_le {d : σ →₀ ℕ} (h : coeff d f ≠ 0) : f.order ≤ degree d :=
  by
  rw [degree_eq_weight_one]
  exact weightedOrder_le _ h

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