radical_le

formal source

 846/-! ### Radical algebra -/
 847
 848/-- rad(n) ≤ n for all n ≠ 0. -/
 849theorem radical_le {n : ℕ} (hn : n ≠ 0) : radical n ≤ n := by
 850  simp only [radical]
 851  have h := Nat.prod_primeFactors_dvd n
 852  exact Nat.le_of_dvd (Nat.pos_of_ne_zero hn) h
 853
 854/-- rad(1) = 1 (using the general definition). -/
 855theorem radical_one_eq : radical 1 = 1 := by native_decide
 856
 857/-- rad(n) > 0 for n > 0. -/
 858theorem radical_pos {n : ℕ} (_hn : 0 < n) : 0 < radical n := by
 859  simp only [radical]
 860  exact Finset.prod_pos (fun p hp => Nat.Prime.pos (Nat.prime_of_mem_primeFactors hp))
 861
 862/-! ### Coprimality power lemmas -/
 863
 864/-- Coprimality is preserved by powers on the left. -/
 865theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
 866    Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b := by
 867  exact Nat.coprime_pow_left_iff hn a b
 868
 869/-- Coprimality is preserved by powers on the right. -/
 870theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
 871    Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b := by
 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