English
Let φ be a formal power series over a semiring R and n an extended natural. If every coefficient with index i, viewed inside the natural numbers, is zero whenever i’s cast is less than n, then n ≤ order φ.
Русский
Пусть φ — формальный степенной ряд над полем R, и n ∈ ENat. Если для каждого i ∈ ℕ выполняется, что iᶜ < n, и коэффициент i φ равен 0, то n ≤ order φ.
LaTeX
$$$\forall \phi \in R\lbrack\!\!X\rbrack,\ n \in \mathbb{N}^{\infty},\ (\forall i:\mathbb{N},\ i^\uparrow < n\Rightarrow coeff_i\,\phi = 0)\ \Rightarrow n \le \operatorname{order}(\phi)$$$
Lean4
/-- The order of a formal power series is at least `n` if
the `i`th coefficient is `0` for all `i < n`. -/
theorem le_order (φ : R⟦X⟧) (n : ℕ∞) (h : ∀ i : ℕ, ↑i < n → coeff i φ = 0) : n ≤ order φ := by
cases n with
| top => simpa using ext (by simpa using h)
| coe n =>
convert nat_le_order φ n _
simpa using h
