Commit 2026-10-17 12:17 bf4d31d2

chore(RingTheory/Pochhammer): fix the type of ascPochhammer_eval_succ (#42827) The existing two theorems have the following signature

theorem ascPochhammer_nat_eval_succ (r n : ℕ) : 
    n * Polynomial.eval (n + 1) (ascPochhammer ℕ r) = (n + r) * Polynomial.eval n (ascPochhammer ℕ r)
theorem ascPochhammer_eval_succ (S : Type*) [Semiring S] (r n : ℕ) : 
    ↑n * Polynomial.eval (↑n + 1) (ascPochhammer S r) = (↑n + ↑r) * Polynomial.eval (↑n) (ascPochhammer S r)

However what's more useful in practice is the following

theorem ascPochhammer_eval_succ {S : Type*} [Semiring S] (r : ℕ) (n : S) : 
    n * Polynomial.eval (n + 1) (ascPochhammer S r) =  Polynomial.eval n (ascPochhammer S r) * (n + ↑r)

which this PR proves. Note that the multiplication order is changed so it doesn't require commutativity on S. The old ascPochhammer_nat_eval_succ is now a specialization of the new ascPochhammer_eval_succ with S = ℕ & mul_comm, so it is redundant, thus deprecated.