mathlib

0f6eec63 - feat(ring_theory/polynomial/pochhammer): generalize a proof from `comm_semiring` to `semiring` (#13024)

feat(ring_theory/polynomial/pochhammer): generalize a proof from `comm_semiring` to `semiring` (#13024) This PR is similar to #13018. Lemma `pochhammer_succ_eval` was already proven with a commutativity assumption. I generalized the proof to `semiring` by introducing a helper lemma. I still feel that this is harder than I would like it to be: `pochhammer` "is" a polynomial in `ℕ[X]` and all these commutativity assumptions are satisfied, since `ℕ[X]` is commutative.