Commit 2023-03-09 06:58 bb982b64

View on Github →

feat: port RingTheory.Polynomial.Pochhammer (#2733)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem Polynomial.mul_x_add_nat_cast_comp

added theorem factorial_mul_pochhammer

added theorem pochhammer_eval_cast

added theorem pochhammer_eval_one

added theorem pochhammer_eval_succ

added theorem pochhammer_eval_zero

added theorem pochhammer_map

added theorem pochhammer_mul

added theorem pochhammer_nat_eq_ascFactorial

added theorem pochhammer_nat_eq_descFactorial

added theorem pochhammer_nat_eval_succ

added theorem pochhammer_ne_zero_eval_zero

added theorem pochhammer_one

added theorem pochhammer_pos

added theorem pochhammer_succ_comp_x_add_one

added theorem pochhammer_succ_eval

added theorem pochhammer_succ_left

added theorem pochhammer_succ_right

added theorem pochhammer_zero

added theorem pochhammer_zero_eval_zero