English
For any nonzero f ∈ k⟦X⟧, the leading coefficient after removing the largest X-power divisor is a unit of k; this yields a distinguished unit firstUnitCoeff f.
Русский
Для любого f ≠ 0 в k⟦X⟧ ведущий коэффициент после выделения наибольшего множителя X является единицей поля k; это задаёт особый элемент единицы firstUnitCoeff f.
LaTeX
$$$ \forall f \in k\langle\langle X\rangle\rangle,\ f \neq 0 \Rightarrow IsUnit( constantCoeff(divXPowOrder f) ). $$$
Lean4
/-- `firstUnitCoeff` is the non-zero coefficient whose index is `f.order`, seen as a unit of the
field. It is obtained using `divided_by_X_pow_order`, defined in `PowerSeries.Order`. -/
def firstUnitCoeff {f : k⟦X⟧} (hf : f ≠ 0) : kˣ :=
have : Invertible (constantCoeff (divXPowOrder f)) :=
by
apply invertibleOfNonzero
simpa [constantCoeff_divXPowOrder_eq_zero_iff.not]
unitOfInvertible (constantCoeff (divXPowOrder f))
