## Stream: Is there code for X?

### Topic: integer polynomials

#### Kevin Buzzard (Dec 29 2020 at 14:01):

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 (Dec 29 2020 at 14:32):

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

#### Adam Topaz (Dec 29 2020 at 14:35):

They're not really the pochhammer symbols are they?

#### Kevin Buzzard (Dec 29 2020 at 17:23):

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

Last updated: May 17 2021 at 16:26 UTC