English
For DecidableEq σ, coeff n (invOfUnit φ u) equals if n = 0 then ↑u⁻¹ else -↑u⁻¹ × ∑_{x ∈ antidiagonal n} coeff x.1 φ × coeff x.2 (invOfUnit φ u).
Русский
Для DecidableEq σ коэффициент n (invOfUnit φ u) равен: если n = 0, то ↑u⁻¹, иначе -↑u⁻¹ × сумма по антидиагонали n коэффициентов φ и invOfUnit φ u.
LaTeX
$$$ coeff\ n\ (invOfUnit\ φ\ u) = \begin{cases} ↑u^{-1}, & n=0 \\ -↑u^{-1} \cdot \sum_{x \in antidiagonal\ n} (coeff x.1\ φ) \cdot (coeff x.2 (invOfUnit φ u)), & \text{иначе} \end{cases}$$$
Lean4
theorem coeff_inv [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) :
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 :=
coeff_inv_aux n _ φ
