# mathlibdocumentation

ring_theory.polynomial.pochhammer

# The Pochhammer polynomials #

We define and prove some basic relations about pochhammer S n : S[X] := X * (X + 1) * ... * (X + n - 1) which is also known as the rising factorial. A version of this definition that is focused on nat can be found in data.nat.factorial as nat.asc_factorial.

## Implementation #

As with many other families of polynomials, even though the coefficients are always in ℕ, we define the polynomial with coefficients in any [semiring S].

## TODO #

There is lots more in this direction:

• q-factorials, q-binomials, q-Pochhammer.
noncomputable def pochhammer (S : Type u) [semiring S] :

pochhammer S n is the polynomial X * (X+1) * ... * (X + n - 1), with coefficients in the semiring S.

Equations
@[simp]
theorem pochhammer_zero (S : Type u) [semiring S] :
0 = 1
@[simp]
theorem pochhammer_one (S : Type u) [semiring S] :
theorem pochhammer_succ_left (S : Type u) [semiring S] (n : ) :
(n + 1) = polynomial.X * n).comp
@[simp]
theorem pochhammer_map {S : Type u} [semiring S] {T : Type v} [semiring T] (f : S →+* T) (n : ) :
n) = n
@[simp, norm_cast]
theorem pochhammer_eval_cast (S : Type u) [semiring S] (n k : ) :
n)) = n)
theorem pochhammer_eval_zero (S : Type u) [semiring S] {n : } :
n) = ite (n = 0) 1 0
theorem pochhammer_zero_eval_zero (S : Type u) [semiring S] :
0) = 1
@[simp]
theorem pochhammer_ne_zero_eval_zero (S : Type u) [semiring S] {n : } (h : n 0) :
n) = 0
theorem pochhammer_succ_right (S : Type u) [semiring S] (n : ) :
(n + 1) = n *
theorem pochhammer_succ_eval {S : Type u_1} [semiring S] (n : ) (k : S) :
(n + 1)) = n) * (k + n)
theorem pochhammer_succ_comp_X_add_one (S : Type u) [semiring S] (n : ) :
(n + 1)).comp = (n + 1) + (n + 1) n).comp
theorem polynomial.mul_X_add_nat_cast_comp (S : Type u) [semiring S] {p q : polynomial S} {n : } :
(p * (polynomial.X + n)).comp q = p.comp q * (q + n)
theorem pochhammer_mul (S : Type u) [semiring S] (n m : ) :
n * m).comp = (n + m)
theorem pochhammer_nat_eq_desc_factorial (a b : ) :
b) = (a + b - 1).desc_factorial b
theorem pochhammer_pos {S : Type u_1} [nontrivial S] (n : ) (s : S) (h : 0 < s) :
0 < n)
@[simp]
theorem pochhammer_eval_one (S : Type u_1) [semiring S] (n : ) :
n) = (n.factorial)
theorem factorial_mul_pochhammer (S : Type u_1) [semiring S] (r n : ) :
theorem pochhammer_nat_eval_succ (r n : ) :
n * polynomial.eval (n + 1) r) = (n + r) * r)
theorem pochhammer_eval_succ (S : Type u_1) [semiring S] (r n : ) :
n * polynomial.eval (n + 1) r) = (n + r) * r)