radical_one_eq

formal source

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