Commit 2020-10-04 15:27 8f536768
View on Github →feat(data/nat): Slightly strengthen nat.coprime_of_dvd/nat.coprime_of_dvd' (#4368) It is sufficient to consider prime factors. The theorems now depend on nat.prime (data/nat/prime.lean), which depends on data/nat/gcd.lean, so I moved them to prime.lean.