radical_thirty

formal source

 832theorem mobius_twelve : mobius 12 = 0 := by native_decide
 833
 834/-- rad(30) = 30 (squarefree). -/
 835theorem radical_thirty : radical 30 = 30 := by native_decide
 836
 837/-- rad(60) = 30. -/
 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 : ℕ) :