Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-20 10:43 504a2dc8

View on Github →

Create choose.lean (#48) deat(data/nat): add choose function to compute the binomial coefficients

Estimated changes

Created data/nat/choose.lean

added def choose

added theorem choose_eq_fact_div_fact

added theorem choose_eq_zero_of_lt

added theorem choose_mul_fact_mul_fact

added theorem choose_one_right

added theorem choose_pos

added theorem choose_self

added theorem choose_succ_self

added theorem choose_succ_succ

added theorem choose_zero_right

added theorem choose_zero_succ

added theorem fact_mul_fact_dvd_fact

added theorem succ_mul_choose_eq