Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 03:59 94aae73d

View on Github →

feat(data/nat/factorial) : descending factorial (#7527)

Estimated changes

Modified src/data/nat/choose/basic.lean

added theorem nat.choose_eq_desc_fac_div_factorial

added theorem nat.desc_fac_eq_factorial_mul_choose

added theorem nat.factorial_dvd_desc_fac

Modified src/data/nat/factorial.lean

added def nat.desc_fac

added theorem nat.desc_fac_eq_div

added theorem nat.desc_fac_succ

added theorem nat.desc_fac_zero

added theorem nat.factorial_mul_desc_fac

added theorem nat.succ_desc_fac

added theorem nat.zero_desc_fac

Modified src/ring_theory/polynomial/bernstein.lean

deleted theorem bernstein_polynomial.iterate_derivative_at_0_aux₁

deleted theorem bernstein_polynomial.iterate_derivative_at_0_aux₂

Modified src/ring_theory/polynomial/pochhammer.lean

deleted theorem choose_eq_pochhammer_eval_div_factorial

deleted theorem factorial_mul_pochhammer'

deleted theorem pochhammer_eval_eq_choose_mul_factorial

deleted theorem pochhammer_eval_eq_factorial_div_factorial

deleted theorem pochhammer_eval_one'

added theorem pochhammer_eval_succ

added theorem pochhammer_nat_eq_desc_fac

added theorem pochhammer_nat_eval_succ