falling factorial as polynomial

Stream: mathlib4

[Moritz Firsching]

We have Pochhammer, which is the rising factorial as polynomial. Wouldn't it be nice to also have falling factorial as a polynomial? (I need it in a proof currently)

What would be a good name? I think it might be a good idea to change pochhammer to raisingFactorial and then add fallingFactorial.
We already have the corresponding ascFactorial and descFactorial for Nat, so if it is too confusing to call the polynomials raisingFactorial and fallingFactorial, one could also go with ascFactorialPolynomial and descFactorialPolynomial or raisingFactorialPolynomial and fallingFactorialPolynomial
I guess one could also simply go with pochhammer and pochhammer'
(or even pochhammer and remmahhcop, just kidding)

What do you think?

[Yaël Dillies]

What about ascPochhammer/descPochhammer?

[Moritz Firsching]

Ok, I made a proposal for ascPochhammer, descPochhammer in #6917 (the rename) and #6918 (adding descPochhammer) , reviews most welcome!