invOneSubPow_val_succ_eq_mk_add_choose

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.invOneSubPow_val_succ_eq_mk_add_choose

English

For d ∈ ℕ, the (d+1)st inverse subpower has coefficients binomial(d+n, d) for all n ≥ 0.

Русский

Для целого d коэффициенты invOneSubPow S (d+1) при n ≥ 0 равны binom(d+n, d).

LaTeX

$$$$ (invOneSubPow\, S\,(d+1)).\text{val} = \mathrm{mk}\, (n \mapsto \binom{d+n}{d}) $$$$

Lean4

theorem invOneSubPow_val_succ_eq_mk_add_choose :
    (invOneSubPow S (d + 1)).val = (mk fun n => Nat.choose (d + n) d : S⟦X⟧) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru