Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.choose_eq_factorial_div_factorial'

Modification history

2021-08-07 20:32
src/data/nat/choose/dvd.lean
refactor(data/nat/choose): reduce assumptions on lemmas (#8508) …
Deleted nat.choose_eq_factorial_div_factorial'View on Github →
2021-02-27 09:13
src/data/nat/choose/dvd.lean
chore(data/nat/choose): fix namespace of theorems (#6451)
Added nat.choose_eq_factorial_div_factorial'View on Github →