theorem
proved
bigOmega_threehundredsixty
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 645.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
642theorem bigOmega_fortyfive : bigOmega 45 = 3 := by native_decide
643
644/-- Ω(360) = 6 (since 360 = 2³ × 3² × 5). -/
645theorem bigOmega_threehundredsixty : bigOmega 360 = 6 := by native_decide
646
647/-- Ω(840) = 6 (since 840 = 2³ × 3 × 5 × 7, with 3+1+1+1 = 6 factors). -/
648theorem bigOmega_eighthundredforty : bigOmega 840 = 6 := by native_decide
649
650/-- ω(8) = 1 (only prime factor is 2). -/
651theorem omega_eight : omega 8 = 1 := by native_decide
652
653/-- ω(45) = 2 (prime factors are 3 and 5). -/
654theorem omega_fortyfive : omega 45 = 2 := by native_decide
655
656/-- ω(360) = 3 (prime factors are 2, 3, 5). -/
657theorem omega_threehundredsixty : omega 360 = 3 := by native_decide
658
659/-- ω(840) = 4 (prime factors are 2, 3, 5, 7). -/
660theorem omega_eighthundredforty : omega 840 = 4 := by native_decide
661
662/-! ### Radical (product of distinct prime factors) -/
663
664/-- The radical of n is the product of its distinct prime factors. -/
665def radical (n : ℕ) : ℕ := n.primeFactors.prod id
666
667/-- rad(1) = 1. -/
668theorem radical_one' : radical 1 = 1 := by native_decide
669
670/-- rad(2) = 2. -/
671theorem radical_two' : radical 2 = 2 := by native_decide
672
673/-- rad(6) = 6 (squarefree). -/
674theorem radical_six' : radical 6 = 6 := by native_decide
675