English
For φ ∈ R[[X]] and n ∈ ENat, the order φ = n if and only if the nth coefficient corresponding to i = n is nonzero and every coefficient with i < n equals zero.
Русский
Для φ ∈ R[[X]] и n ∈ ENat порядок φ равен n тогда и только тогда, когда коэффициент i = n ненулевой, а все коэффициенты с i < n равны нулю.
LaTeX
$$$\operatorname{order}(\phi) = n \iff (\forall i:\mathbb{N},\ i = n \Rightarrow \operatorname{coeff}_i(\phi) \neq 0) \land (\forall i:\mathbb{N},\ i < n \Rightarrow \operatorname{coeff}_i(\phi) = 0)$$$
Lean4
/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
and the `i`th coefficient is `0` for all `i < n`. -/
theorem order_eq {φ : R⟦X⟧} {n : ℕ∞} :
order φ = n ↔ (∀ i : ℕ, ↑i = n → coeff i φ ≠ 0) ∧ ∀ i : ℕ, ↑i < n → coeff i φ = 0 := by
cases n with
| top => simp
| coe n => simp [order_eq_nat]
