English
Let f be a multivariate formal power series with coefficients in a semiring R. Then for every natural number n, the order of f satisfies: ord(f) = n if and only if there exists a coefficient at some degree d with degree(d) = n and coeff d f ≠ 0, and every coefficient at degree less than n vanishes (coeff d f = 0 whenever degree d < n).
Русский
Пусть f — многомерный формальный степенной ряд над полем (кольцом) R. Тогда для каждого натурального числа n порядок f удовлетворяет: ord(f) = n тогда и только тогда, когда существует коэффициент при некотором степени d с degree(d) = n и коэффициент coeff d f ≠ 0, и для всех степеней d с degree(d) < n коэффициент coeff d f = 0.
LaTeX
$$$ \operatorname{ord}(f) = n \iff \big( \exists d : \sigma \to_{0} \mathbb{N}, \operatorname{coeff} d f \neq 0 \land \operatorname{degree} d = n \big) \land \forall d, \operatorname{degree} d < n \rightarrow \operatorname{coeff} d f = 0 $$$
Lean4
/-- The order of a formal power series is exactly `n` some coefficient
of degree `n` is nonzero,
and the `d`th coefficient is `0` for all `d` such that `degree d < n`. -/
theorem order_eq_nat {n : ℕ} : f.order = n ↔ (∃ d, coeff d f ≠ 0 ∧ degree d = n) ∧ ∀ d, degree d < n → coeff d f = 0 :=
by
simp_rw [degree_eq_weight_one]
exact weightedOrder_eq_nat _
