Commit 2023-09-12 12:40 ae1eb5e7

View on Github →

chore: rename pochhammer (#6917) We rename pochhammer to ascPochhammer to prepare adding descPochhammer.

Estimated changes

modified theorem Nat.cast_ascFactorial
modified theorem Nat.cast_descFactorial
modified theorem Nat.cast_factorial
added theorem ascPochhammer_eval_one
added theorem ascPochhammer_map
added theorem ascPochhammer_mul
added theorem ascPochhammer_one
added theorem ascPochhammer_pos
added theorem ascPochhammer_zero
deleted theorem factorial_mul_pochhammer
deleted theorem pochhammer_eval_cast
deleted theorem pochhammer_eval_one
deleted theorem pochhammer_eval_succ
deleted theorem pochhammer_eval_zero
deleted theorem pochhammer_map
deleted theorem pochhammer_mul
deleted theorem pochhammer_nat_eval_succ
deleted theorem pochhammer_one
deleted theorem pochhammer_pos
deleted theorem pochhammer_succ_eval
deleted theorem pochhammer_succ_left
deleted theorem pochhammer_succ_right
deleted theorem pochhammer_zero
deleted theorem pochhammer_zero_eval_zero