coeff_invOfUnit — Mathlib

English

The coefficient at n of invOfUnit φ u is given by the same pattern as coeff_inv_aux, but with a constant term ↑u⁻¹ at n = 0: coeff n (invOfUnit φ u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ · sum over antidiagonal n of coeff x.1 φ · coeff x.2 (invOfUnit φ u).

Русский

Коэффициент при n в invOfUnit φ u задаётся аналогично coeff_inv_aux, но при n = 0 даётся ↑u⁻¹: coeff 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{otherwise} \end{cases}$$$

Lean4

theorem coeff_invOfUnit [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (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 :=
  by convert coeff_inv_aux n (↑u⁻¹) φ

Похожие утверждения