def
definition
radical
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 665.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
affineShift_mem_LevelSet -
dot_affineShift -
radical_integrable_by_affine_leaves -
sub_mem_Radical -
omega_eighthundredforty -
radical_eighthundredforty -
radical_le -
radical_one' -
radical_one_eq -
radical_onehundredtwenty -
radical_pos -
radical_prime' -
radical_prime_pow -
radical_six' -
radical_sixty -
radical_thirty -
radical_threehundredsixty -
radical_twelve' -
radical_two' -
radical_twohundredten -
not_squarefree_840 -
radical_360 -
radical_eight
formal source
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
688/-- φ(n) = |{a ∈ [0,n) : gcd(n,a) = 1}|. -/
689theorem totient_eq_card_filter {n : ℕ} :
690 totient n = (Finset.filter (fun a => n.Coprime a) (Finset.range n)).card := by
691 simp only [totient]
692 exact Nat.totient_eq_card_coprime n
693
694/-! ### Additional coprimality facts for RS constants -/
695