English
DivXPowOrder is the operation that divides out the largest power of X dividing f; i.e., the coefficient of degree n in divXPowOrder f equals the coefficient of degree n+order(f) in f.
Русский
DivXPowOrder — операция деления на наибольшую степень X, делящую f; то есть коэффициент при X^n в divXPowOrder f равен коэффициенту при X^{n+order(f)} в f.
LaTeX
$$$(\operatorname{divXPowOrder} f)\,\text{coeff}_n = \operatorname{coeff}_{n + \operatorname{order}(f)} f$$$
Lean4
/-- Given a non-zero power series `f`, `divXPowOrder f` is the power series obtained by
dividing out the largest power of X that divides `f`, that is its order -/
def divXPowOrder (f : R⟦X⟧) : R⟦X⟧ :=
.mk fun n ↦ coeff (n + f.order.toNat) f
