mathlib3
b7a54188 - feat(data/nat/gcd/basic): add `nat.dvd_mul` and `dvd_mul` (#17131)

Commit
3 years ago
feat(data/nat/gcd/basic): add `nat.dvd_mul` and `dvd_mul` (#17131) This follows trivially from `prod_dvd_and_dvd_of_dvd_prod` and `exists_dvd_and_dvd_of_dvd_mul`, but is more discoverable and easier to use. Also fixes some bad indentation in the same file.
Author
Parents
Loading