mathlib3 documentation

ring_theory.polynomial.pochhammer

The Pochhammer polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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] :
@[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, norm_cast]
theorem pochhammer_eval_zero (S : Type u) [semiring S] {n : } :
polynomial.eval 0 (pochhammer S n) = ite (n = 0) 1 0
@[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 pochhammer_succ_eval {S : Type u_1} [semiring S] (n : ) (k : S) :
theorem pochhammer_succ_comp_X_add_one (S : Type u) [semiring S] (n : ) :
(pochhammer S (n + 1)).comp (polynomial.X + 1) = pochhammer S (n + 1) + (n + 1) (pochhammer S n).comp (polynomial.X + 1)
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} [strict_ordered_semiring 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 : ) :
theorem pochhammer_eval_succ (S : Type u_1) [semiring S] (r n : ) :