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)
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)