factorial_nsmul_multichoose_eq_ascPochhammer

English

Let r be an element of a binomial ring R and n a natural number. Then n! multiplied by multichoose r n equals the smeval of ascPochhammer ℕ n evaluated at r: n! · multichoose r n = (ascPochhammer ℕ n).smeval r.

Русский

Пусть r принадлежит биномиальному кольцу R, а n — натуральное число. Тогда n! · multichoose r n = (ascPochhammer ℕ n).smeval r.

LaTeX

$$$n! \cdot multichoose\; r\; n = (ascPochhammer\; \mathbb{N}\; n).smeval\; r$$$

Lean4

theorem factorial_nsmul_multichoose_eq_ascPochhammer (r : R) (n : ℕ) :
    n.factorial • multichoose r n = (ascPochhammer ℕ n).smeval r :=
  BinomialRing.factorial_nsmul_multichoose r n

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