English
For any nonzero polynomial P, the count of X in the power-series normalization of P equals the count of X in the polynomial normalization of P.
Русский
Для любого ненулевого многочлена P число X в нормализованных разложениях P в виде степенного ряда равно числу X в нормализованных разложениях P как многочлена.
LaTeX
$$Multiset.count(PowerSeries.X)(normalizedFactors(P)) = Multiset.count(Polynomial.X)(normalizedFactors(P))$$
Lean4
/-- The order of a formal power series `φ` is the greatest `n : PartENat`
such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`. -/
def order (φ : R⟦X⟧) : ℕ∞ :=
letI := Classical.decEq R
letI := Classical.decEq R⟦X⟧
if h : φ = 0 then ⊤ else Nat.find (exists_coeff_ne_zero_iff_ne_zero.mpr h)
