Theorems · Definition · number theory
Nat.descFactorial
ℕ → ℕ → ℕ
n.descFactorial k = n! / (n - k)! (as seen in Nat.descFactorial_eq_div), but
implemented recursively to allow for "quick" computation when using norm_num. This is closely
related to descPochhammer, but much less general.
- Defined in
- Mathlib.Data.Nat.Factorial.Basic
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by69
Results whose statement or proof uses this declaration.
- Nat.descFactorial_eq_factorial_mul_choosestatement and proof · cited by 12
- Nat.descFactorial_eq_zero_iff_ltstatement · cited by 9
- Nat.descFactorial_succstatement · cited by 9
- Nat.choose_eq_descFactorial_div_factorialstatement · cited by 5
- Nat.descFactorial_zerostatement · cited by 5
- Nat.descFactorial_le_powstatement · cited by 4
- Polynomial.iterate_derivative_X_sub_powstatement and proof · cited by 4
- Nat.descFactorial_selfstatement · cited by 3
- Nat.factorial_mul_descFactorialstatement · cited by 3
- descPochhammer_eval_eq_descFactorialstatement and proof · cited by 3
- ascPochhammer_nat_eq_descFactorialstatement and proof · cited by 3
- Polynomial.iterate_derivative_mul_X_powstatement and proof · cited by 3