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 to 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 .
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