English
The nth coefficient of invOfUnit φ u is equal to u^{-1} if n=0, and otherwise equals -u^{-1} times the sum over the antidiagonal n of coeff x φ times coeff x' (invOfUnit φ u) with a suitable selection if x'.2 < n.
Русский
n-й коэффициент invOfUnit φ u равен u^{-1} при n=0, иначе равен -u^{-1} умножить на сумму по антидиагонали n из coeff x φ умножить на coeff x' (invOfUnit φ u) при условии x'.2 < n.
LaTeX
$$$ \operatorname{coeff}_n(\operatorname{invOfUnit} φ u) = \begin{cases} ↑u^{-1}, & n = 0 \\ -↑u^{-1} \cdot \sum_{x \in \operatorname{antidiagonal} n} \operatorname{coeff}_{x.1} φ \cdot \operatorname{coeff}_{x.2}(\operatorname{invOfUnit} φ u), & n>0 \end{cases} $$$
Lean4
theorem coeff_invOfUnit (n : ℕ) (φ : R⟦X⟧) (u : Rˣ) :
coeff n (invOfUnit φ u) =
if n = 0 then ↑u⁻¹
else -↑u⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then coeff x.1 φ * coeff x.2 (invOfUnit φ u) else 0 :=
coeff_inv_aux n (↑u⁻¹ : R) φ
