Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 17:21 80d688e3

View on Github →

feat(data/nat/choose): nat.prime.dvd_choose (#419)

  • feat(data/nat/choose): nat/prime.dvd_choose
  • use nat namespace
  • Update prime.lean
  • improve readability

Estimated changes

added theorem nat.prime.dvd_choose
added theorem nat.prime.dvd_fact