binomialSeries_coeff — Mathlib

English

For a binomial series with coefficient r in R, the nth coefficient equals Ring.choose r n.

Русский

Для биномиального ряда коэффициент при n-том члене равен choose r n.

LaTeX

$$$\\operatorname{coeff}_n(\\text{binomialSeries } A r) = \\operatorname{Ring.choose} r n$$$

Lean4

@[simp]
theorem binomialSeries_coeff [Semiring A] [SMul R A] (r : R) (n : ℕ) :
    coeff n (binomialSeries A r) = Ring.choose r n • 1 :=
  coeff_mk n fun n ↦ Ring.choose r n • 1

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