`omega_threehundredsixty`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 657 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 657.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

formal source

 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
 676/-- rad(12) = 6. -/
 677theorem radical_twelve' : radical 12 = 6 := by native_decide
 678
 679/-- rad(p) = p for prime p. -/
 680theorem radical_prime' {p : ℕ} (hp : Prime p) : radical p = p := by
 681  have hp' : Nat.Prime p := (prime_iff p).1 hp
 682  simp only [radical]
 683  rw [Nat.Prime.primeFactors hp']
 684  simp
 685
 686/-! ### Totient as cardinality -/
 687

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.