theorem
proved
radical_two'
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 671.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
696/-- gcd(8, 360) = 8. -/
697theorem gcd_eight_threehundredsixty : Nat.gcd 8 360 = 8 := by native_decide
698
699/-- gcd(45, 360) = 45. -/
700theorem gcd_fortyfive_threehundredsixty : Nat.gcd 45 360 = 45 := by native_decide
701