English
For a field k and φ ∈ k⟦X⟧, the coefficient of φ⁻¹ is given by if n=0 then (constantCoeff φ)⁻¹, otherwise - (constantCoeff φ)⁻¹ times the sum over the antidiagonal of coeff x φ times coeff x' φ⁻¹, with the appropriate condition.
Русский
Для поля k и φ ∈ k⟦X⟧ коэффициент φ⁻¹ задаётся как: если n=0, то (const φ)⁻¹, иначе - (const φ)⁻¹ умножить на сумму по антидиагонали.
LaTeX
$$$ \operatorname{coeff}_n(φ^{-1}) = \begin{cases} (\mathrm{constantCoeff } φ)^{-1}, & n=0 \\ - (\mathrm{constantCoeff } φ)^{-1} \cdot \sum_{x \in \operatorname{antidiagonal} n} \mathrm{coeff}_{x.1} φ \cdot \mathrm{coeff}_{x.2}(φ^{-1}), & n>0 \end{cases} $$$
Lean4
theorem coeff_inv (n) (φ : k⟦X⟧) :
coeff n φ⁻¹ =
if n = 0 then (constantCoeff φ)⁻¹
else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then coeff x.1 φ * coeff x.2 φ⁻¹ else 0 :=
by rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff φ)⁻¹ φ]
