English
For nonzero f, the unit formed by dividing by the largest X-power is a unit with the value divXPowOrder f and corresponding inverse Inv_divided_by_X_pow_order hf, i.e., a canonical unit in k⟦X⟧.
Русский
Для непустого f единичный элемент, полученный делением на наибольшую степень X, имеет значение divXPowOrder f и обратное Inv_divided_by_X_pow_order hf, то есть каноническая единица в k⟦X⟧.
LaTeX
$$$ Unit\_of\_divided\_by\_X\_pow\_order(f)\; :\; (val := divXPowOrder(f), inv := Inv\_divided\_by\_X\_pow\_order(hf), ...) $$$
Lean4
/-- `Unit_of_divided_by_X_pow_order` is the unit power series obtained by dividing a non-zero
power series by the largest power of `X` that divides it. -/
def Unit_of_divided_by_X_pow_order (f : k⟦X⟧) : k⟦X⟧ˣ :=
if hf : f = 0 then 1
else
{ val := divXPowOrder f
inv := Inv_divided_by_X_pow_order hf
val_inv := Inv_divided_by_X_pow_order_rightInv hf
inv_val := Inv_divided_by_X_pow_order_leftInv hf }
