mathlib documentation

ring_theory.polynomial.pochhammer

The Pochhammer polynomials #

We define and prove some basic relations about pochhammer S n : polynomial S = X * (X+1) * ... * (X + n - 1) which is also known as the rising 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:

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] :
@[simp]
theorem pochhammer_one (S : Type u) [semiring S] :
theorem pochhammer_succ_left (S : Type u) [semiring S] (n : ) :
@[simp]
theorem pochhammer_map {S : Type u} [semiring S] {T : Type v} [semiring T] (f : S →+* T) (n : ) :
@[simp]
theorem pochhammer_eval_cast (S : Type u) [semiring S] (n k : ) :
theorem pochhammer_eval_zero (S : Type u) [semiring S] {n : } :
polynomial.eval 0 (pochhammer S n) = ite (n = 0) 1 0
theorem pochhammer_zero_eval_zero (S : Type u) [semiring S] :
@[simp]
theorem pochhammer_ne_zero_eval_zero (S : Type u) [semiring S] {n : } (h : n 0) :
theorem pochhammer_succ_right (S : Type u) [semiring S] (n : ) :
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 : ) :
theorem pochhammer_pos {S : Type u_1} [ordered_semiring S] [nontrivial S] (n : ) (s : S) (h : 0 < s) :
@[simp]
theorem pochhammer_eval_one (S : Type u_1) [semiring S] (n : ) :
theorem factorial_mul_pochhammer (S : Type u_1) [semiring S] (r n : ) :
(r!) * polynomial.eval (r + 1) (pochhammer S n) = (r + n)!
theorem pochhammer_eval_succ (S : Type u_1) [semiring S] (r n : ) :