English
The order of a formal power series φ is exactly n if and only if the nth coefficient is nonzero and all coefficients with smaller indices are zero.
Русский
Порядок ряда φ равен точно n тогда и только тогда, когда коэффициент при X^n ненулевой, а коэффициенты при X^i для i < n равны нулю.
LaTeX
$$$\operatorname{order}(\phi) = n \iff \left( \operatorname{coeff}_n(\phi) \neq 0 \land \forall i < n,\ operatorname{coeff}_i(\phi) = 0 \right)$$$
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_nat {φ : R⟦X⟧} {n : ℕ} : order φ = n ↔ coeff n φ ≠ 0 ∧ ∀ i, i < n → coeff i φ = 0 := by
classical
rcases eq_or_ne φ 0 with (rfl | hφ)
· simp
simp [order, dif_neg hφ, Nat.find_eq_iff]
