ascPochhammer_nat_eq_descFactorial

English

For natural a,b, ascPochhammer Nat b evaluated at a equals (a+b-1).descFactorial b.

Русский

Для натуральных a,b: ascPochhammer Nat b, когда оценивается в a, равно (a+b−1).descFactorial b.

LaTeX

$$$(ascPochhammer\\ Nat\\ b).\\mathrm{eval}\\ a = (a + b - 1).\\mathrm{descFactorial}\\ b$$$

Lean4

theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) : (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

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