mathlib3

7a37490c - feat(ring_theory/polynomial/pochhammer): add a binomial like recursion for pochhammer (#13018)

feat(ring_theory/polynomial/pochhammer): add a binomial like recursion for pochhammer (#13018) This PR proves the identity `pochhammer R n + n * (pochhammer R (n - 1)).comp (X + 1) = (pochhammer R n).comp (X + 1)` analogous to the additive recursion for binomial coefficients. For the proof, first we prove the result for a `comm_semiring` as `pochhammer_add_pochhammer_aux`. Next, we apply this identity in the general case. If someone has any idea of how to make the maths statement: it suffices to show this identity for pochhammer symbols in the commutative case, I would be *very* happy to know!