Commit 2022-12-17 08:57 4a230a9b

View on Github →

feat port: Data.Nat.Choose.Basic (#1073) d012cd09a9b256d870751284dd6a29882b0be105

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Choose/Basic.lean

added theorem Nat.add_choose

added theorem Nat.add_choose_mul_factorial_mul_factorial

added theorem Nat.ascFactorial_eq_factorial_mul_choose

added def Nat.choose

added theorem Nat.choose_eq_asc_factorial_div_factorial

added theorem Nat.choose_eq_descFactorial_div_factorial

added theorem Nat.choose_eq_factorial_div_factorial

added theorem Nat.choose_eq_zero_iff

added theorem Nat.choose_eq_zero_of_lt

added theorem Nat.choose_le_add

added theorem Nat.choose_le_choose

added theorem Nat.choose_le_middle

added theorem Nat.choose_le_succ

added theorem Nat.choose_le_succ_of_lt_half_left

added theorem Nat.choose_mono

added theorem Nat.choose_mul

added theorem Nat.choose_mul_factorial_mul_factorial

added theorem Nat.choose_mul_succ_eq

added theorem Nat.choose_one_right

added theorem Nat.choose_pos

added theorem Nat.choose_self

added theorem Nat.choose_succ_right_eq

added theorem Nat.choose_succ_self

added theorem Nat.choose_succ_self_right

added theorem Nat.choose_succ_succ

added theorem Nat.choose_symm

added theorem Nat.choose_symm_add

added theorem Nat.choose_symm_half

added theorem Nat.choose_symm_of_eq_add

added theorem Nat.choose_two_right

added theorem Nat.choose_zero_right

added theorem Nat.choose_zero_succ

added theorem Nat.descFactorial_eq_factorial_mul_choose

added theorem Nat.factorial_dvd_ascFactorial

added theorem Nat.factorial_dvd_descFactorial

added theorem Nat.factorial_mul_factorial_dvd_factorial

added theorem Nat.factorial_mul_factorial_dvd_factorial_add

added def Nat.multichoose

added theorem Nat.multichoose_eq

added theorem Nat.multichoose_one

added theorem Nat.multichoose_one_right

added theorem Nat.multichoose_succ_succ

added theorem Nat.multichoose_two

added theorem Nat.multichoose_zero_right

added theorem Nat.multichoose_zero_succ

added theorem Nat.succ_mul_choose_eq

added theorem Nat.triangle_succ