English
Let φ be a formal power series over a semiring R. If all coefficients up to index n−1 vanish (coeff i φ = 0 for every i < n), then the order of φ is at least n. In particular, ↑n ≤ order φ.
Русский
Пусть φ — формальный степенной ряд над полем/кольцом R. Если все коэффициенты при X^i для i < n равны нулю, то порядок φ не меньше n. То есть ↑n ≤ order φ.
LaTeX
$$$\forall \phi \in R\lbrack\!\!X\rbrack,\ \forall n \in \mathbb{N},\ (\forall i < n,\ coeff_i\,\phi = 0)\ \Rightarrow \uparrow 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 nat_le_order (φ : R⟦X⟧) (n : ℕ) (h : ∀ i < n, coeff i φ = 0) : ↑n ≤ order φ := by
classical
simp only [order]
split_ifs
· simp
· simpa [Nat.le_find_iff]
