invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos

English

If d > 0, the nth coefficient of invOneSubPow S d is binomial(d − 1 + n, d − 1).

Русский

Если d > 0, коэффициент при X^n у invOneSubPow S d равен биномиальному числу binom(d − 1 + n, d − 1).

LaTeX

$$$$ 0 < d \Rightarrow \text{coeff}_n\big( invOneSubPow\, S\, d \big) = \binom{d-1+n}{d-1} $$$$

Lean4

theorem invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos (h : 0 < d) :
    (invOneSubPow S d).val = (mk fun n => Nat.choose (d - 1 + n) (d - 1) : S⟦X⟧) := by
  rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]

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