Basic

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

Statistics

Metric	Count
Definitions `fast_choose`, `multichoose`	2
Theorems `add_choose`, `add_choose_mul_factorial_mul_factorial`, `add_one_mul_choose_eq`, `ascFactorial_eq_factorial_mul_choose`, `ascFactorial_eq_factorial_mul_choose'`, `choose_eq_asc_factorial_div_factorial`, `choose_eq_asc_factorial_div_factorial'`, `choose_eq_choose_pred_add`, `choose_eq_descFactorial_div_factorial`, `choose_eq_factorial_div_factorial`, `choose_eq_fast_choose`, `choose_eq_one_iff`, `choose_eq_zero_iff`, `choose_eq_zero_of_lt`, `choose_le_add`, `choose_le_choose`, `choose_le_middle`, `choose_le_succ`, `choose_le_succ_of_lt_half_left`, `choose_mono`, `choose_mul`, `choose_mul_add`, `choose_mul_factorial_mul_factorial`, `choose_mul_right`, `choose_mul_succ_eq`, `choose_ne_zero`, `choose_ne_zero_iff`, `choose_one_right`, `choose_pos`, `choose_self`, `choose_succ_left`, `choose_succ_right`, `choose_succ_right_eq`, `choose_succ_self`, `choose_succ_self_right`, `choose_succ_succ`, `choose_succ_succ'`, `choose_symm`, `choose_symm_add`, `choose_symm_half`, `choose_symm_of_eq_add`, `choose_two_right`, `choose_zero_right`, `choose_zero_succ`, `descFactorial_eq_factorial_mul_choose`, `factorial_dvd_ascFactorial`, `factorial_dvd_descFactorial`, `factorial_mul_factorial_dvd_factorial`, `factorial_mul_factorial_dvd_factorial_add`, `multichoose_eq`, `multichoose_one`, `multichoose_one_right`, `multichoose_succ_succ`, `multichoose_two`, `multichoose_zero_right`, `multichoose_zero_succ`, `succ_mul_choose_eq`, `triangle_succ`	58
Total	60

Nat

Definitions

Name	Category	Theorems
`fast_choose` 📖	CompOp	1 math math: `choose_eq_fast_choose`
`multichoose` 📖	CompOp	12 math math: `sum_range_multichoose`, `multichoose_one`, `multichoose_succ_succ`, `List.length_sym`, `multichoose_zero_succ`, `multichoose_zero_right`, `Sym.card_sym_fin_eq_multichoose`, `multichoose_eq`, `multichoose_two`, `Finset.card_finsuppAntidiag_nat_eq_multichoose`, `multichoose_one_right`, `Sym.card_sym_eq_multichoose`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_choose` 📖	mathematical	—	`choose` `factorial`	—	`choose_eq_factorial_div_factorial`
`add_choose_mul_factorial_mul_factorial` 📖	mathematical	—	`choose` `factorial`	—	`choose_mul_factorial_mul_factorial`
`add_one_mul_choose_eq` 📖	mathematical	—	`choose`	—	`choose_zero_right` `choose_one_right` `choose_succ_succ'`
`ascFactorial_eq_factorial_mul_choose` 📖	mathematical	—	`ascFactorial` `factorial` `choose`	—	`factorial_pos` `choose_mul_factorial_mul_factorial` `factorial_mul_ascFactorial`
`ascFactorial_eq_factorial_mul_choose'` 📖	mathematical	—	`ascFactorial` `factorial` `choose`	—	`ascFactorial_zero` `choose_zero_right` `factorial_zero` `zero_ascFactorial` `choose_succ_self` `ascFactorial_eq_factorial_mul_choose`
`choose_eq_asc_factorial_div_factorial` 📖	mathematical	—	`choose` `ascFactorial` `factorial`	—	`factorial_pos` `ascFactorial_eq_factorial_mul_choose` `factorial_dvd_ascFactorial`
`choose_eq_asc_factorial_div_factorial'` 📖	mathematical	—	`choose` `ascFactorial` `factorial`	—	`factorial_ne_zero` `ascFactorial_eq_factorial_mul_choose'`
`choose_eq_choose_pred_add` 📖	mathematical	—	`choose`	—	`choose_succ_right`
`choose_eq_descFactorial_div_factorial` 📖	mathematical	—	`choose` `descFactorial` `factorial`	—	`factorial_ne_zero` `descFactorial_eq_factorial_mul_choose`
`choose_eq_factorial_div_factorial` 📖	mathematical	—	`choose` `factorial`	—	`choose_mul_factorial_mul_factorial` `factorial_pos`
`choose_eq_fast_choose` 📖	mathematical	—	`choose` `fast_choose`	—	`choose_eq_descFactorial_div_factorial`
`choose_eq_one_iff` 📖	mathematical	—	`choose`	—	`lt_trichotomy` `choose_self`
`choose_eq_zero_iff` 📖	mathematical	—	`choose`	—	`lt_of_not_ge` `choose_pos` `Eq.not_lt` `choose_eq_zero_of_lt`
`choose_eq_zero_of_lt` 📖	mathematical	—	`choose`	—	`choose_zero_succ` `choose_succ_succ`
`choose_le_add` 📖	mathematical	—	`choose`	—	`LE.le.trans` `choose_le_succ`
`choose_le_choose` 📖	mathematical	—	`choose`	—	`choose_le_add`
`choose_le_middle` 📖	mathematical	—	`choose`	—	`le_or_gt` `choose_symm` `choose_eq_zero_of_lt`
`choose_le_succ` 📖	mathematical	—	`choose`	—	—
`choose_le_succ_of_lt_half_left` 📖	mathematical	—	`choose`	—	`choose_succ_right_eq` `lt_of_lt_of_le` `LT.lt.trans_le`
`choose_mono` 📖	mathematical	—	`Monotone` `instPreorder` `choose`	—	`choose_le_choose`
`choose_mul` 📖	mathematical	—	`choose`	—	`lt_or_ge` `factorial_pos`
`choose_mul_add` 📖	mathematical	—	`choose`	—	`factorial_ne_zero` `add_choose_mul_factorial_mul_factorial` `factorial_succ`
`choose_mul_factorial_mul_factorial` 📖	mathematical	—	`choose` `factorial`	—	`choose_self` `choose_zero_right` `lt_or_eq_of_le` `factorial_succ` `choose_succ_succ` `choose_succ_self`
`choose_mul_right` 📖	mathematical	—	`choose`	—	`choose_mul_add`
`choose_mul_succ_eq` 📖	mathematical	—	`choose`	—	`choose_zero_right` `le_or_gt` `choose_succ_succ` `choose_succ_right_eq` `choose_eq_zero_of_lt` `LT.lt.trans`
`choose_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `choose_pos`
`choose_ne_zero_iff` 📖	—	—	—	—	`not_iff_not`
`choose_one_right` 📖	mathematical	—	`choose`	—	`choose_zero_right`
`choose_pos` 📖	mathematical	—	`choose`	—	`choose_zero_right`
`choose_self` 📖	mathematical	—	`choose`	—	—
`choose_succ_left` 📖	mathematical	—	`choose`	—	—
`choose_succ_right` 📖	mathematical	—	`choose`	—	—
`choose_succ_right_eq` 📖	mathematical	—	`choose`	—	`choose_succ_succ` `add_one_mul_choose_eq`
`choose_succ_self` 📖	mathematical	—	`choose`	—	`choose_eq_zero_of_lt`
`choose_succ_self_right` 📖	mathematical	—	`choose`	—	`choose_succ_succ` `choose_self`
`choose_succ_succ` 📖	mathematical	—	`choose`	—	—
`choose_succ_succ'` 📖	mathematical	—	`choose`	—	—
`choose_symm` 📖	mathematical	—	`choose`	—	`choose_eq_factorial_div_factorial`
`choose_symm_add` 📖	mathematical	—	`choose`	—	`choose_symm_of_eq_add`
`choose_symm_half` 📖	mathematical	—	`choose`	—	`choose_symm_of_eq_add`
`choose_symm_of_eq_add` 📖	mathematical	—	`choose`	—	`choose_symm`
`choose_two_right` 📖	mathematical	—	`choose`	—	`triangle_succ` `choose.eq_3` `choose_one_right`
`choose_zero_right` 📖	mathematical	—	`choose`	—	—
`choose_zero_succ` 📖	mathematical	—	`choose`	—	—
`descFactorial_eq_factorial_mul_choose` 📖	mathematical	—	`descFactorial` `factorial` `choose`	—	`descFactorial_eq_zero_iff_lt` `choose_eq_zero_of_lt` `factorial_pos` `choose_mul_factorial_mul_factorial` `factorial_mul_descFactorial`
`factorial_dvd_ascFactorial` 📖	mathematical	—	`factorial` `ascFactorial`	—	`ascFactorial_eq_factorial_mul_choose'`
`factorial_dvd_descFactorial` 📖	mathematical	—	`factorial` `descFactorial`	—	`descFactorial_eq_factorial_mul_choose`
`factorial_mul_factorial_dvd_factorial` 📖	mathematical	—	`factorial`	—	`choose_mul_factorial_mul_factorial`
`factorial_mul_factorial_dvd_factorial_add` 📖	mathematical	—	`factorial`	—	`factorial_mul_factorial_dvd_factorial`
`multichoose_eq` 📖	mathematical	—	`multichoose` `choose`	—	—
`multichoose_one` 📖	mathematical	—	`multichoose`	—	`multichoose_zero_right` `multichoose_succ_succ` `multichoose_zero_succ`
`multichoose_one_right` 📖	mathematical	—	`multichoose`	—	`multichoose_zero_succ` `multichoose_succ_succ` `multichoose_zero_right`
`multichoose_succ_succ` 📖	mathematical	—	`multichoose`	—	`multichoose.eq_3`
`multichoose_two` 📖	mathematical	—	`multichoose`	—	`multichoose_zero_right` `multichoose.eq_3` `multichoose_one`
`multichoose_zero_right` 📖	mathematical	—	`multichoose`	—	`multichoose.eq_1`
`multichoose_zero_succ` 📖	mathematical	—	`multichoose`	—	`multichoose.eq_2`
`succ_mul_choose_eq` 📖	mathematical	—	`choose`	—	`add_one_mul_choose_eq`
`triangle_succ` 📖	—	—	—	—	—

---

← Back to Index