Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-27 09:13 7256361a

View on Github →

chore(data/nat/choose): fix namespace of theorems (#6451)

Estimated changes

Modified src/data/nat/choose/dvd.lean

added theorem nat.choose_eq_factorial_div_factorial'

added theorem nat.choose_mul

deleted theorem nat.prime.choose_eq_factorial_div_factorial'

deleted theorem nat.prime.choose_mul