theorem
proved
mobius_thirty
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 829.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
826theorem mobius_six : mobius 6 = 1 := by native_decide
827
828/-- μ(30) = -1 (squarefree with 3 prime factors). -/
829theorem mobius_thirty : mobius 30 = -1 := by native_decide
830
831/-- μ(12) = 0 (not squarefree, since 4 | 12). -/
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]