Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-18 13:38 18217e9a

View on Github →

feat(nat/choose): Generalise nat.dvd_choose (#2703) Spin-off from #2701.

Estimated changes

Modified src/algebra/char_p.lean

Modified src/data/nat/choose.lean

deleted theorem nat.prime.dvd_choose

added theorem nat.prime.dvd_choose_add

added theorem nat.prime.dvd_choose_self

modified theorem sum_range_choose