Algebraic identities for ascending Pochhammer symbols

These multiplicative identities avoid division by parameter-dependent factors, so they remain valid at zeros of the Pochhammer symbols.

theorem ascPochhammer_eval_shift {R : Type u_1} [CommSemiring R] (p : R) (n : ℕ) : p * Polynomial.eval (p + 1) (ascPochhammer R n) = (p + ↑n) * Polynomial.eval p (ascPochhammer R n)

A division-free shift identity for ascending Pochhammer symbols.

theorem ascPochhammer_add_eval {R : Type u_1} [CommSemiring R] (p : R) (n m : ℕ) : Polynomial.eval p (ascPochhammer R (n + m)) = Polynomial.eval p (ascPochhammer R n) * Polynomial.eval (p + ↑n) (ascPochhammer R m)

Evaluation of the product formula for ascending Pochhammer symbols.

theorem ascPochhammer_eval_double {R : Type u_1} [Field R] [CharZero R] (p : R) (n : ℕ) : Polynomial.eval (2 * p) (ascPochhammer R (2 * n)) = 4 ^ n * Polynomial.eval p (ascPochhammer R n) * Polynomial.eval (p + 1 / 2) (ascPochhammer R n)

Duplication of ascending Pochhammer symbols, in division-free multiplicative form.

theorem ascPochhammer_eval_split_reflect {R : Type u_1} [CommRing R] (c : R) {m n : ℕ} (hmn : m ≤ n) : Polynomial.eval c (ascPochhammer R n) = (-1) ^ (n - m) * Polynomial.eval c (ascPochhammer R m) * Polynomial.eval (1 - c - ↑n) (ascPochhammer R (n - m))

Splitting an ascending Pochhammer symbol and reflecting the remaining factors.

The multiplicative form remains valid when one of the Pochhammer factors vanishes, unlike the corresponding quotient identity.

theorem ascPochhammer_eval_reflect {R : Type u_1} [CommRing R] (p : R) (n : ℕ) : Polynomial.eval (1 - p - ↑n) (ascPochhammer R n) = (-1) ^ n * Polynomial.eval p (ascPochhammer R n)

Reflection of ascending Pochhammer symbols, including their zeros.