∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ),
  (MvPowerSeries.coeff n) (φ.invOfUnit u) =
    if n = 0 then ↑u⁻¹
    else
      -↑u⁻¹ *
        ∑ x ∈ Finset.antidiagonal n,
          if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (φ.invOfUnit u) else 0