English
In the ring of formal power series S[[X]], the inverse of (1 − X)^d is the power series whose coefficients are binomial(d − 1 + n, d − 1) for d > 0; when d = 0 the inverse is 1.
Русский
В кольце формальных степенных рядов S[[X]] обратка (1 − X)^d имеет коэффициенты binom(d − 1 + n, d − 1) при d > 0; при d = 0 обратная равна 1.
LaTeX
$$$$ invOneSubPow\, S\, d = \begin{cases} 1, & d = 0, \\\n\mathrm{mk}\, (n \mapsto \binom{d-1+n}{d-1}), & d > 0. \end{cases} $$$$
Lean4
/-- Given a natural number `d : ℕ` and a commutative ring `S`, `PowerSeries.invOneSubPow S d` is the
multiplicative inverse of `(1 - X) ^ d` in `S⟦X⟧ˣ`. When `d` is `0`, `PowerSeries.invOneSubPow S d`
will just be `1`. When `d` is positive, `PowerSeries.invOneSubPow S d` will be the power series
`mk fun n => Nat.choose (d - 1 + n) (d - 1)`.
-/
noncomputable def invOneSubPow : ℕ → S⟦X⟧ˣ
| 0 => 1
| d + 1 =>
{ val := mk fun n => Nat.choose (d + n) d
inv := (1 - X) ^ (d + 1)
val_inv := by rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
inv_val := by rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow] }
