radical_threehundredsixty

formal source

 838theorem radical_sixty : radical 60 = 30 := by native_decide
 839
 840/-- rad(360) = 30. -/
 841theorem radical_threehundredsixty : radical 360 = 30 := by native_decide
 842
 843/-- rad(840) = 210 = 2 × 3 × 5 × 7. -/
 844theorem radical_eighthundredforty : radical 840 = 210 := by native_decide
 845
 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