integer polynomials

Stream: Is there code for X?

[Kevin Buzzard]

My obsession with Bernoulli numbers turned to an obsession with how to work with the function sending $(i,j)$ to $\frac{(i+j)!}{i!j!}$ and is now coming around to the idea of pascal (n : ℕ) : polynomial ℚ := (∏ i in finset.range n, (polynomial.X + i)) / n!. These functions are a basis for integer-valued polynomials and I guess there is even a nat-valued statement: nat-valued polynomials are nat-linear combinations of these, all happening as subgroups of polynomial rat. Do we have these in Lean? What is the name of these fuctions in other languages? In mathematics? Oh -- https://en.wikipedia.org/wiki/Falling_and_rising_factorials . pockhammer? upperfact?

[Adam Topaz]

https://en.wikipedia.org/wiki/Binomial_transform might be useful

[Adam Topaz]

They're not really the pochhammer symbols are they?

[Kevin Buzzard]

the wikipedia link mentioned his name as being associated with them.