sigma_one_threehundredsixty

formal source

 735theorem sigma_one_fortyfive : sigma 1 45 = 78 := by native_decide
 736
 737/-- σ_1(360) = 1170. -/
 738theorem sigma_one_threehundredsixty : sigma 1 360 = 1170 := by native_decide
 739
 740/-! ### Prime factors of primes and prime powers -/
 741
 742/-- The prime factors of a prime p is just {p}. -/
 743theorem primeFactors_prime {p : ℕ} (hp : Prime p) : p.primeFactors = {p} := by
 744  have hp' : Nat.Prime p := (prime_iff p).1 hp
 745  exact Nat.Prime.primeFactors hp'
 746
 747/-- The prime factors of p^k (k ≥ 1) is just {p}. -/
 748theorem primeFactors_prime_pow {p k : ℕ} (hp : Prime p) (hk : k ≠ 0) :
 749    (p ^ k).primeFactors = {p} := by
 750  have hp' : Nat.Prime p := (prime_iff p).1 hp
 751  exact Nat.primeFactors_prime_pow hk hp'
 752
 753/-- rad(p^k) = p for prime p and k ≥ 1. -/
 754theorem radical_prime_pow {p k : ℕ} (hp : Prime p) (hk : k ≠ 0) : radical (p ^ k) = p := by
 755  simp only [radical, primeFactors_prime_pow hp hk, Finset.prod_singleton, id]
 756
 757/-! ### Von Mangoldt sum identity -/
 758
 759/-- The sum of von Mangoldt over divisors: ∑_{d|n} Λ(d) = log(n).
 760    This connects Λ to the logarithm. -/
 761theorem vonMangoldt_sum_divisors {n : ℕ} :
 762    ∑ d ∈ n.divisors, vonMangoldt d = Real.log n := by
 763  simp only [vonMangoldt]
 764  exact ArithmeticFunction.vonMangoldt_sum
 765
 766/-! ### Sigma multiplicativity helpers -/
 767
 768/-- σ_k(mn) = σ_k(m) × σ_k(n) for coprime m, n. -/