coprime_pow_of_prime_not_dvd

formal source

 872  exact Nat.coprime_pow_right_iff hn a b
 873
 874/-- If p is prime and doesn't divide a, then a is coprime to p^m. -/
 875theorem coprime_pow_of_prime_not_dvd {p m a : ℕ} (hp : Prime p) (h : ¬p ∣ a) :
 876    Nat.Coprime a (p ^ m) := by
 877  have hp' : Nat.Prime p := (prime_iff p).1 hp
 878  exact hp'.coprime_pow_of_not_dvd h
 879
 880/-- Two distinct primes raised to powers are coprime. -/
 881theorem coprime_prime_pow {p q n m : ℕ} (hp : Prime p) (hq : Prime q) (hne : p ≠ q) :
 882    Nat.Coprime (p ^ n) (q ^ m) := by
 883  have hp' : Nat.Prime p := (prime_iff p).1 hp
 884  have hq' : Nat.Prime q := (prime_iff q).1 hq
 885  exact Nat.coprime_pow_primes n m hp' hq' hne
 886
 887/-! ### More primeCounting values -/
 888
 889/-- π(150) = 35. -/
 890theorem primeCounting_onehundredfifty : primeCounting 150 = 35 := by native_decide
 891
 892/-- π(250) = 53. -/
 893theorem primeCounting_twohundredfifty : primeCounting 250 = 53 := by native_decide
 894
 895/-- π(500) = 95. -/
 896theorem primeCounting_fivehundred : primeCounting 500 = 95 := by native_decide
 897
 898/-- π(750) = 132. -/
 899theorem primeCounting_sevenhundredfifty : primeCounting 750 = 132 := by native_decide
 900
 901/-! ### Legendre formula concrete values -/
 902
 903/-- vp 2 (10!) = 8. -/
 904theorem vp_factorial_ten_two : vp 2 (Nat.factorial 10) = 8 := by native_decide
 905