Basic

📁 Source: Mathlib/Data/Nat/Factorial/Basic.lean

Statistics

Metric	Count
Definitions `ascFactorial`, `ascFactorialBinary`, `descFactorial`, `descFactorialBinary`, `factorialBinarySplitting`, `prodRange`, `term_!`	7
Theorems `add_descFactorial_eq_ascFactorial`, `add_descFactorial_eq_ascFactorial'`, `add_factorial_le_factorial_add`, `add_factorial_lt_factorial_add`, `add_factorial_succ_le_factorial_add_succ`, `add_factorial_succ_lt_factorial_add_succ`, `ascFactorial_eq_ascFactorialBinary`, `ascFactorial_eq_div`, `ascFactorial_eq_div'`, `ascFactorial_le_pow_add`, `ascFactorial_lt_pow_add`, `ascFactorial_mul_ascFactorial`, `ascFactorial_of_sub`, `ascFactorial_pos`, `ascFactorial_succ`, `ascFactorial_zero`, `descFactorial_eq_descFactorialBinary`, `descFactorial_eq_div`, `descFactorial_eq_zero_iff_lt`, `descFactorial_le`, `descFactorial_le_pow`, `descFactorial_lt_pow`, `descFactorial_mul_descFactorial`, `descFactorial_of_lt`, `descFactorial_one`, `descFactorial_pos`, `descFactorial_self`, `descFactorial_succ`, `descFactorial_zero`, `dvd_factorial`, `factorial_mul_prodRange`, `factorialBinarySplitting_eq_factorial`, `factorial_dvd_factorial`, `factorial_eq_factorialBinarySplitting`, `factorial_eq_one`, `factorial_inj`, `factorial_inj'`, `factorial_le`, `factorial_le_pow`, `factorial_lt`, `factorial_lt_of_lt`, `factorial_mul_ascFactorial`, `factorial_mul_ascFactorial'`, `factorial_mul_descFactorial`, `factorial_mul_pow_le_factorial`, `factorial_mul_pow_sub_le_factorial`, `factorial_ne_zero`, `factorial_one`, `factorial_pos`, `factorial_succ`, `factorial_two`, `factorial_two_mul_le`, `factorial_zero`, `lt_factorial_self`, `mul_factorial_pred`, `one_ascFactorial`, `one_lt_factorial`, `pow_lt_ascFactorial`, `pow_lt_ascFactorial'`, `pow_sub_le_descFactorial`, `pow_sub_lt_descFactorial`, `pow_sub_lt_descFactorial'`, `pow_succ_le_ascFactorial`, `self_le_factorial`, `succ_ascFactorial`, `succ_descFactorial`, `succ_descFactorial_succ`, `two_pow_mul_factorial_le_factorial_two_mul`, `zero_ascFactorial`, `zero_descFactorial_succ`	70
Total	77

Nat

Definitions

Name	Category	Theorems
`ascFactorial` 📖	CompOp	31 math math: `factorial_mul_ascFactorial`, `choose_eq_asc_factorial_div_factorial'`, `factorial_dvd_ascFactorial`, `ascFactorial_pos`, `cast_ascFactorial`, `ascFactorial_lt_pow_add`, `ascFactorial_zero`, `ascFactorial_succ`, `one_ascFactorial`, `ascFactorial_eq_factorial_mul_choose'`, `ascFactorial_eq_div'`, `ascFactorial_eq_prod_range`, `descPochhammer_int_eq_ascFactorial`, `numDerangements_sum`, `zero_ascFactorial`, `ascFactorial_eq_div`, `pow_succ_le_ascFactorial`, `choose_eq_asc_factorial_div_factorial`, `ascFactorial_of_sub`, `ascFactorial_eq_factorial_mul_choose`, `ascFactorial_le_pow_add`, `ascFactorial_eq_ascFactorialBinary`, `add_descFactorial_eq_ascFactorial'`, `ascPochhammer_nat_eq_natCast_ascFactorial`, `factorial_mul_ascFactorial'`, `add_descFactorial_eq_ascFactorial`, `pow_lt_ascFactorial'`, `ascPochhammer_nat_eq_ascFactorial`, `ascFactorial_mul_ascFactorial`, `pow_lt_ascFactorial`, `succ_ascFactorial`
`ascFactorialBinary` 📖	CompOp	1 math math: `ascFactorial_eq_ascFactorialBinary`
`descFactorial` 📖	CompOp	54 math math: `isEquivalent_descFactorial`, `descFactorial_one`, `cast_descFactorial_two`, `iteratedDeriv_pow`, `Polynomial.iterate_derivative_X_add_pow`, `descFactorial_of_lt`, `ascPochhammer_nat_eq_descFactorial`, `Polynomial.iterate_derivative_X_sub_pow`, `descFactorial_lt_pow`, `descFactorial_pos`, `Mathlib.Meta.NormNum.isNat_descFactorial`, `Polynomial.descPochhammer_smeval_eq_descFactorial`, `ascPochhammer_nat_eq_natCast_descFactorial`, `descPochhammer_eval_le_sum_descFactorial`, `pow_sub_lt_descFactorial`, `Polynomial.iterate_derivative_X_pow_eq_natCast_mul`, `pow_sub_le_descFactorial`, `zero_descFactorial_succ`, `summable_descFactorial_mul_geometric_of_norm_lt_one`, `Polynomial.iterate_derivative_X_pow_eq_smul`, `Polynomial.iterate_derivative_eq_sum`, `descFactorial_succ`, `descFactorial_eq_div`, `choose_lt_descFactorial`, `Mathlib.Meta.NormNum.isNat_descFactorial_zero`, `factorial_dvd_descFactorial`, `iteratedDerivWithin_pow`, `descPochhammer_eval_eq_descFactorial`, `ContinuousMultilinearMap.norm_iteratedFDeriv_le`, `Polynomial.coeff_iterate_derivative`, `ContinuousMultilinearMap.norm_iteratedFDeriv_le'`, `descFactorial_eq_prod_range`, `ZMod.cast_descFactorial`, `Polynomial.iterate_derivative_mul_X_pow`, `Polynomial.iterate_derivative_X_pow_eq_C_mul`, `descFactorial_le_pow`, `descFactorial_le`, `add_descFactorial_eq_ascFactorial'`, `descFactorial_eq_zero_iff_lt`, `descFactorial_eq_descFactorialBinary`, `descFactorial_self`, `descFactorial_zero`, `pow_sub_lt_descFactorial'`, `add_descFactorial_eq_ascFactorial`, `choose_eq_descFactorial_div_factorial`, `descFactorial_eq_factorial_mul_choose`, `descFactorial_mul_descFactorial`, `choose_le_descFactorial`, `Prime.coprime_descFactorial_of_lt_of_le`, `Fintype.card_embedding_eq`, `cast_descFactorial`, `succ_descFactorial`, `factorial_mul_descFactorial`, `succ_descFactorial_succ`
`descFactorialBinary` 📖	CompOp	1 math math: `descFactorial_eq_descFactorialBinary`
`factorialBinarySplitting` 📖	CompOp	2 math math: `factorial_eq_factorialBinarySplitting`, `factorialBinarySplitting_eq_factorial`
`term_!` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_descFactorial_eq_ascFactorial` 📖	mathematical	—	`descFactorial` `ascFactorial`	—	`ascFactorial_zero` `descFactorial_zero` `succ_descFactorial_succ` `ascFactorial_succ`
`add_descFactorial_eq_ascFactorial'` 📖	mathematical	—	`descFactorial` `ascFactorial`	—	`ascFactorial_zero` `descFactorial_zero` `descFactorial_succ` `ascFactorial_succ` `succ_ascFactorial`
`add_factorial_le_factorial_add` 📖	mathematical	—	`factorial`	—	`self_le_factorial` `add_factorial_succ_le_factorial_add_succ`
`add_factorial_lt_factorial_add` 📖	mathematical	—	`factorial`	—	`factorial_one` `lt_factorial_self` `add_factorial_succ_lt_factorial_add_succ`
`add_factorial_succ_le_factorial_add_succ` 📖	mathematical	—	`factorial`	—	`le_or_gt` `add_factorial_succ_lt_factorial_add_succ` `factorial_succ` `factorial_pos`
`add_factorial_succ_lt_factorial_add_succ` 📖	mathematical	—	`factorial`	—	`factorial_succ` `self_le_factorial` `factorial_le`
`ascFactorial_eq_ascFactorialBinary` 📖	mathematical	—	`ascFactorial` `ascFactorialBinary`	—	`ascFactorialBinary.induct_unfolding`
`ascFactorial_eq_div` 📖	mathematical	—	`ascFactorial` `factorial`	—	`factorial_ne_zero` `factorial_mul_ascFactorial`
`ascFactorial_eq_div'` 📖	mathematical	—	`ascFactorial` `factorial`	—	`factorial_ne_zero` `factorial_mul_ascFactorial'`
`ascFactorial_le_pow_add` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial_zero` `le_refl` `ascFactorial_succ`
`ascFactorial_lt_pow_add` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial_succ` `le_refl` `ascFactorial_le_pow_add`
`ascFactorial_mul_ascFactorial` 📖	mathematical	—	`ascFactorial`	—	`zero_ascFactorial` `factorial_pos` `factorial_mul_ascFactorial`
`ascFactorial_of_sub` 📖	mathematical	—	`ascFactorial`	—	`succ_ascFactorial` `ascFactorial_succ`
`ascFactorial_pos` 📖	mathematical	—	`ascFactorial`	—	`pow_succ_le_ascFactorial`
`ascFactorial_succ` 📖	mathematical	—	`ascFactorial`	—	—
`ascFactorial_zero` 📖	mathematical	—	`ascFactorial`	—	—
`descFactorial_eq_descFactorialBinary` 📖	mathematical	—	`descFactorial` `descFactorialBinary`	—	`descFactorialBinary.eq_1` `descFactorial_of_lt` `ascFactorial_eq_ascFactorialBinary` `add_descFactorial_eq_ascFactorial'`
`descFactorial_eq_div` 📖	mathematical	—	`descFactorial` `factorial`	—	`factorial_pos` `factorial_mul_descFactorial` `factorial_dvd_factorial`
`descFactorial_eq_zero_iff_lt` 📖	mathematical	—	`descFactorial`	—	`descFactorial_succ`
`descFactorial_le` 📖	mathematical	—	`descFactorial`	—	`le_refl` `descFactorial_succ`
`descFactorial_le_pow` 📖	mathematical	—	`descFactorial`	—	`descFactorial_zero` `le_refl` `descFactorial_succ`
`descFactorial_lt_pow` 📖	mathematical	—	`descFactorial`	—	`descFactorial_succ` `descFactorial_le_pow`
`descFactorial_mul_descFactorial` 📖	mathematical	—	`descFactorial`	—	`factorial_pos` `factorial_mul_descFactorial` `le_trans` `descFactorial_eq_zero_iff_lt`
`descFactorial_of_lt` 📖	mathematical	—	`descFactorial`	—	`descFactorial_eq_zero_iff_lt`
`descFactorial_one` 📖	mathematical	—	`descFactorial`	—	—
`descFactorial_pos` 📖	mathematical	—	`descFactorial`	—	—
`descFactorial_self` 📖	mathematical	—	`descFactorial` `factorial`	—	`descFactorial_zero` `factorial_zero` `succ_descFactorial_succ` `factorial_succ`
`descFactorial_succ` 📖	mathematical	—	`descFactorial`	—	—
`descFactorial_zero` 📖	mathematical	—	`descFactorial`	—	—
`dvd_factorial` 📖	mathematical	—	`factorial`	—	`factorial_dvd_factorial`
`factorialBinarySplitting_eq_factorial` 📖	mathematical	—	`factorial` `factorialBinarySplitting`	—	`factorial_eq_factorialBinarySplitting`
`factorial_dvd_factorial` 📖	mathematical	—	`factorial`	—	—
`factorial_eq_factorialBinarySplitting` 📖	mathematical	—	`factorial` `factorialBinarySplitting`	—	`one_ascFactorial`
`factorial_eq_one` 📖	mathematical	—	`factorial`	—	`not_lt` `one_lt_factorial` `lt_irrefl`
`factorial_inj` 📖	mathematical	—	`factorial`	—	`lt_trichotomy` `lt_irrefl` `factorial_lt` `one_lt_factorial`
`factorial_inj'` 📖	mathematical	—	`factorial`	—	—
`factorial_le` 📖	mathematical	—	`factorial`	—	`factorial_pos` `factorial_dvd_factorial`
`factorial_le_pow` 📖	mathematical	—	`factorial`	—	`le_refl`
`factorial_lt` 📖	mathematical	—	`factorial`	—	`not_le` `factorial_le` `factorial_succ` `factorial_pos` `lt_trans`
`factorial_lt_of_lt` 📖	mathematical	—	`factorial`	—	`factorial_lt`
`factorial_mul_ascFactorial` 📖	mathematical	—	`factorial` `ascFactorial`	—	`ascFactorial_zero` `ascFactorial_succ` `factorial_succ`
`factorial_mul_ascFactorial'` 📖	mathematical	—	`factorial` `ascFactorial`	—	`factorial_mul_ascFactorial`
`factorial_mul_descFactorial` 📖	mathematical	—	`factorial` `descFactorial`	—	`descFactorial_zero` `succ_descFactorial_succ` `factorial_succ`
`factorial_mul_pow_le_factorial` 📖	mathematical	—	`factorial`	—	`factorial_succ`
`factorial_mul_pow_sub_le_factorial` 📖	mathematical	—	`factorial`	—	`factorial_mul_pow_le_factorial`
`factorial_ne_zero` 📖	—	—	—	—	`factorial_pos`
`factorial_one` 📖	mathematical	—	`factorial`	—	—
`factorial_pos` 📖	mathematical	—	`factorial`	—	—
`factorial_succ` 📖	mathematical	—	`factorial`	—	—
`factorial_two` 📖	mathematical	—	`factorial`	—	—
`factorial_two_mul_le` 📖	mathematical	—	`factorial`	—	`factorial_mul_ascFactorial` `ascFactorial_le_pow_add`
`factorial_zero` 📖	mathematical	—	`factorial`	—	—
`lt_factorial_self` 📖	mathematical	—	`factorial`	—	`factorial_succ` `self_le_factorial`
`mul_factorial_pred` 📖	mathematical	—	`factorial`	—	—
`one_ascFactorial` 📖	mathematical	—	`ascFactorial` `factorial`	—	`ascFactorial_zero` `ascFactorial_succ` `factorial_succ`
`one_lt_factorial` 📖	mathematical	—	`factorial`	—	`factorial_lt`
`pow_lt_ascFactorial` 📖	mathematical	—	`ascFactorial`	—	`pow_lt_ascFactorial'`
`pow_lt_ascFactorial'` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial.eq_2` `pow_succ_le_ascFactorial`
`pow_sub_le_descFactorial` 📖	mathematical	—	`descFactorial`	—	`descFactorial_zero` `le_refl` `descFactorial_succ` `le_trans`
`pow_sub_lt_descFactorial` 📖	mathematical	—	`descFactorial`	—	`pow_sub_lt_descFactorial'`
`pow_sub_lt_descFactorial'` 📖	mathematical	—	`descFactorial`	—	`descFactorial_succ` `descFactorial_one`
`pow_succ_le_ascFactorial` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial_zero` `le_refl` `ascFactorial_succ` `succ_ascFactorial`
`self_le_factorial` 📖	mathematical	—	`factorial`	—	`factorial_pos`
`succ_ascFactorial` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial_zero` `ascFactorial.eq_2`
`succ_descFactorial` 📖	mathematical	—	`descFactorial`	—	`descFactorial_zero` `descFactorial.eq_2` `descFactorial_succ`
`succ_descFactorial_succ` 📖	mathematical	—	`descFactorial`	—	`descFactorial_zero` `descFactorial_one` `descFactorial_succ`
`two_pow_mul_factorial_le_factorial_two_mul` 📖	mathematical	—	`factorial`	—	`factorial_mul_pow_le_factorial`
`zero_ascFactorial` 📖	mathematical	—	`ascFactorial`	—	`ascFactorial_succ` `ascFactorial_zero`
`zero_descFactorial_succ` 📖	mathematical	—	`descFactorial`	—	`descFactorial_succ`

Nat.factorialBinarySplitting

Definitions

Name	Category	Theorems
`prodRange` 📖	CompOp	1 math math: `factorial_mul_prodRange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factorial_mul_prodRange` 📖	mathematical	—	`Nat.factorial` `prodRange`	—	`prodRange.eq_1` `Nat.ascFactorial_eq_ascFactorialBinary` `Nat.factorial_mul_ascFactorial`

---

← Back to Index