# Documentation

Mathlib.RingTheory.Polynomial.Pochhammer

# The Pochhammer polynomials #

We define and prove some basic relations about ascPochhammer S n : S[X] := X * (X + 1) * ... * (X + n - 1) which is also known as the rising factorial and about descPochhammer R n : R[X] := X * (X - 1) * ... * (X - n + 1) which is also known as the falling factorial. Versions of this definition that are focused on Nat can be found in Data.Nat.Factorial as Nat.ascFactorial and Nat.descFactorial.

## Implementation #

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

## TODO #

There is lots more in this direction:

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

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

Equations
Instances For
@[simp]
theorem ascPochhammer_zero (S : Type u) [] :
= 1
@[simp]
theorem ascPochhammer_one (S : Type u) [] :
= Polynomial.X
theorem ascPochhammer_succ_left (S : Type u) [] (n : ) :
ascPochhammer S (n + 1) = Polynomial.X * Polynomial.comp () (Polynomial.X + 1)
theorem monic_ascPochhammer (S : Type u) [] (n : ) [] [] :
@[simp]
theorem ascPochhammer_map {S : Type u} [] {T : Type v} [] (f : S →+* T) (n : ) :
@[simp]
theorem ascPochhammer_eval_cast (S : Type u) [] (n : ) (k : ) :
↑() = Polynomial.eval (k) ()
theorem ascPochhammer_eval_zero (S : Type u) [] {n : } :
Polynomial.eval 0 () = if n = 0 then 1 else 0
@[simp]
theorem ascPochhammer_ne_zero_eval_zero (S : Type u) [] {n : } (h : n 0) :
theorem ascPochhammer_succ_right (S : Type u) [] (n : ) :
ascPochhammer S (n + 1) = * (Polynomial.X + n)
theorem ascPochhammer_succ_eval {S : Type u_1} [] (n : ) (k : S) :
Polynomial.eval k (ascPochhammer S (n + 1)) = Polynomial.eval k () * (k + n)
theorem ascPochhammer_succ_comp_X_add_one (S : Type u) [] (n : ) :
Polynomial.comp (ascPochhammer S (n + 1)) (Polynomial.X + 1) = ascPochhammer S (n + 1) + (n + 1) Polynomial.comp () (Polynomial.X + 1)
theorem ascPochhammer_mul (S : Type u) [] (n : ) (m : ) :
* Polynomial.comp () (Polynomial.X + n) = ascPochhammer S (n + m)
@[simp]
theorem ascPochhammer_natDegree (S : Type u) [] (n : ) [] [] :
theorem ascPochhammer_pos {S : Type u_1} (n : ) (s : S) (h : 0 < s) :
@[simp]
theorem ascPochhammer_eval_one (S : Type u_2) [] (n : ) :
Polynomial.eval 1 () = ↑()
theorem factorial_mul_ascPochhammer (S : Type u_2) [] (r : ) (n : ) :
↑() * Polynomial.eval (r + 1) () = ↑(Nat.factorial (r + n))
theorem ascPochhammer_nat_eval_succ (r : ) (n : ) :
n * Polynomial.eval (n + 1) () = (n + r) *
theorem ascPochhammer_eval_succ (S : Type u_1) [] (r : ) (n : ) :
n * Polynomial.eval (n + 1) () = (n + r) * Polynomial.eval (n) ()
noncomputable def descPochhammer (R : Type u) [Ring R] :

descPochhammer R n is the polynomial X * (X - 1) * ... * (X - n + 1), with coefficients in the ring R.

Equations
Instances For
@[simp]
theorem descPochhammer_zero (R : Type u) [Ring R] :
= 1
@[simp]
theorem descPochhammer_one (R : Type u) [Ring R] :
= Polynomial.X
theorem descPochhammer_succ_left (R : Type u) [Ring R] (n : ) :
descPochhammer R (n + 1) = Polynomial.X * Polynomial.comp () (Polynomial.X - 1)
theorem monic_descPochhammer (R : Type u) [Ring R] (n : ) [] [] :
@[simp]
theorem descPochhammer_map {R : Type u} [Ring R] {T : Type v} [Ring T] (f : R →+* T) (n : ) :
@[simp]
theorem descPochhammer_eval_cast (R : Type u) [Ring R] (n : ) (k : ) :
↑() = Polynomial.eval (k) ()
theorem descPochhammer_eval_zero (R : Type u) [Ring R] {n : } :
= if n = 0 then 1 else 0
@[simp]
theorem descPochhammer_ne_zero_eval_zero (R : Type u) [Ring R] {n : } (h : n 0) :
= 0
theorem descPochhammer_succ_right (R : Type u) [Ring R] (n : ) :
descPochhammer R (n + 1) = * (Polynomial.X - n)
@[simp]
theorem descPochhammer_natDegree (R : Type u) [Ring R] (n : ) [] [] :
theorem descPochhammer_succ_eval {S : Type u_1} [Ring S] (n : ) (k : S) :
Polynomial.eval k (descPochhammer S (n + 1)) = * (k - n)
theorem descPochhammer_succ_comp_X_sub_one (R : Type u) [Ring R] (n : ) :
Polynomial.comp (descPochhammer R (n + 1)) (Polynomial.X - 1) = descPochhammer R (n + 1) - (n + 1) Polynomial.comp () (Polynomial.X - 1)
theorem descPochhammer_mul (R : Type u) [Ring R] (n : ) (m : ) :
* Polynomial.comp () (Polynomial.X - n) = descPochhammer R (n + m)
theorem descPochhammer_int_eq_ascFactorial (a : ) (b : ) :
Polynomial.eval (a + b) () = ↑()