mathlib

798c61ba - feat(data/nat/prime): eq_prime_pow_of_dvd_least_prime_pow (#2791)

feat(data/nat/prime): eq_prime_pow_of_dvd_least_prime_pow (#2791) Proves ```lean lemma eq_prime_pow_of_dvd_least_prime_pow (a p k : ℕ) (pp : prime p) (h₁ : ¬(a ∣ p^k)) (h₂ : a ∣ p^(k+1)) : a = p^(k+1) ```