English
For any ring R, the evaluation at −r of ascPochhammer R k equals (−1)^k times the evaluation of descPochhammer R k at r.
Русский
Для кольца R оценка ascPochhammer R k в −r равна (-1)^k умножить на оценку descPochhammer R k в r.
LaTeX
$$$(\operatorname{ascPochhammer} R k).eval(-r) = (-1)^k \cdot (\operatorname{descPochhammer} R k).eval(r)$$$
Lean4
theorem ascPochhammer_eval_neg_eq_descPochhammer (r : R) :
∀ (k : ℕ), (ascPochhammer R k).eval (-r) = (-1) ^ k * (descPochhammer R k).eval r
| 0 => by
rw [ascPochhammer_zero, descPochhammer_zero]
simp only [eval_one, pow_zero, mul_one]
| (k + 1) => by
rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul, Nat.cast_comm, ←
mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc, descPochhammer_succ_right, mul_sub, eval_sub,
eval_mul_X, ← Nat.cast_comm, eval_natCast_mul, pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul,
neg_mul_eq_mul_neg, Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
