Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 12:11 798c61ba

View on Github →

feat(data/nat/prime): eq_prime_pow_of_dvd_least_prime_pow (#2791) Proves

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)

Estimated changes