nat_le_order — Mathlib

English

For n ∈ ℕ, if certain conditions hold, then n ≤ f.order.

Русский

Для натурального n, при выполнении условий, n ≤ order(f).

LaTeX

$$∀ n ∈ ℕ, h → 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 nat_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 nat_le_weightedOrder _ h

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