English
For a semiring S and a,b ∈ Nat, a.descFactorial b equals the evaluation of the ascPochhammer S b at a − (b−1) cast into S.
Русский
Для полупредика S и чисел a,b натуральных, a↓b равно вычислению ascPochhammer S b в элементе a−(b−1), приведённом к S.
LaTeX
$$a.descFactorial b = (ascPochhammer S b).eval (a - (b - 1) : S)$$
Lean4
theorem cast_descFactorial : a.descFactorial b = (ascPochhammer S b).eval (a - (b - 1) : S) :=
by
rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]
induction b with
| zero => simp
| succ b =>
simp_rw [add_succ, Nat.add_one_sub_one]
obtain h | h := le_total a b
· rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
rw [tsub_eq_zero_iff_le.mpr h, zero_add]
· rw [tsub_add_cancel_of_le h]
