order_le — Mathlib

English

If the nth coefficient is nonzero, then order φ ≤ n.

Русский

Если коэффициент при n-ом порядке не ноль, то order φ ≤ n.

LaTeX

$$order(φ) ≤ n if coeff(n, φ) ≠ 0$$

Lean4

/-- If the `n`th coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to `n`. -/
theorem order_le (n : ℕ) (h : coeff n φ ≠ 0) : order φ ≤ n := by
  classical
  rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

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