Commit 2023-09-14 11:42 42093ba3

View on Github →

feat: descPochhammer (#6918)

depends on: #6917

Estimated changes

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.eval₂_at_int_cast

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem Pochhammer_int_eq_descFactorial

added theorem Polynomial.mul_X_sub_int_cast_comp

added theorem descPochhammer_eval_cast

added theorem descPochhammer_eval_zero

added theorem descPochhammer_int_eq_ascFactorial

added theorem descPochhammer_map

added theorem descPochhammer_mul

added theorem descPochhammer_ne_zero_eval_zero

added theorem descPochhammer_one

added theorem descPochhammer_succ_comp_X_sub_one

added theorem descPochhammer_succ_eval

added theorem descPochhammer_succ_left

added theorem descPochhammer_succ_right

added theorem descPochhammer_zero

added theorem descPochhammer_zero_eval_zero