factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473)

Commit

3 years ago

chore(data/nat/factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473) Golfing the edge-case proof added in https://github.com/leanprover-community/mathlib/pull/13316

Author

stuart-presnell

Parents

d89160b5

mathlib3 fd08afe3 - chore(data/nat/factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473)

mathlib3
fd08afe3 - chore(data/nat/factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473)