mk_add_choose_mul_one_sub_pow_eq_one

English

The series with coefficients binom(d+n, d) is the inverse of (1 − X)^{d+1} in the unit group of power series.

Русский

Ряд со коэффициентами {binom(d+n, d)} является обратной к (1 − X)^{d+1} в группе единиц формальных рядов.

LaTeX

$$$$ (\sum_{n=0}^{\infty} \binom{d+n}{d} X^n) \cdot (1 - X)^{d+1} = 1 $$$$

Lean4

theorem mk_add_choose_mul_one_sub_pow_eq_one : (mk fun n ↦ Nat.choose (d + n) d : S⟦X⟧) * ((1 - X) ^ (d + 1)) = 1 :=
  (invOneSubPow S (d + 1)).val_inv

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