theorem
proved
bigOmega_twelve
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 814.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
811theorem omega_six : omega 6 = 2 := by native_decide
812
813/-- Ω(12) = 3 (since 12 = 2² × 3). -/
814theorem bigOmega_twelve : bigOmega 12 = 3 := by native_decide
815
816/-- ω(12) = 2 (distinct prime factors: 2, 3). -/
817theorem omega_twelve : omega 12 = 2 := by native_decide
818
819/-- Ω(30) = 3 (since 30 = 2 × 3 × 5). -/
820theorem bigOmega_thirty : bigOmega 30 = 3 := by native_decide
821
822/-- ω(30) = 3 (distinct prime factors: 2, 3, 5). -/
823theorem omega_thirty : omega 30 = 3 := by native_decide
824
825/-- μ(6) = 1 (squarefree with 2 prime factors). -/
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