English
For DecidableEq σ, for n ∈ σ →₀ ℕ, a ∈ R, φ ∈ MvPowerSeries σ R, the coefficient at n of inv.aux a φ satisfies a recursion: coeff n (inv.aux a φ) = if n = 0 then a else -a · sum over antidiagonal n of coeff x.1 φ · coeff x.2 (inv.aux a φ) with the inner condition x.2 < n.
Русский
Для декапарантного множества σ и n ∈ σ →₀ ℕ коэффициент при n в inv.aux a φ удовлетворяет рекурсии: coeff n (inv.aux a φ) = если n = 0, то a; иначе -a · сумма по антидиагонали n коэффициентов φ и коэффициентов inv.aux a φ.
LaTeX
$$$ coeff\; n\; (inv.aux\ a\ φ) =\begin{cases} a, & n=0 \\ -a \cdot \sum_{x \in antidiagonal\ n} (coeff\ x.1\ φ) \cdot (coeff\ x.2\ (inv.aux a φ)), & \text{otherwise} \end{cases}$$$
Lean4
theorem coeff_inv_aux [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) :
coeff n (inv.aux a φ) =
if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then coeff x.1 φ * coeff x.2 (inv.aux a φ) else 0 :=
show inv.aux a φ n = _ by
cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ)
rw [inv.aux]
rfl
