English
For every n, smeval of ascPochhammer ℕ n evaluated at −n equals (−1)^n · n!.
Русский
Для каждого n, smeval ascPochhammer ℕ n в точке −n равно (−1)^n · n!.
LaTeX
$$$\mathrm{smeval}(\mathrm{ascPochhammer} \mathbb{N} n)(-n) = (-1)^n \; n!$$$
Lean4
@[simp]
theorem smeval_ascPochhammer_self_neg : ∀ n : ℕ, smeval (ascPochhammer ℕ n) (-n : ℤ) = (-1) ^ n * n.factorial
| 0 => by
rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero, one_smul, pow_zero,
Nat.cast_one, one_mul]
| n + 1 => by
rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one, pow_zero, pow_one,
one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm, smeval_ascPochhammer_self_neg n, ←
mul_assoc, mul_comm _ ((-1) ^ n), show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by cutsat, ← mul_assoc, pow_add, pow_one,
Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]
