sigma_zero_eight

formal source

 720/-! ### Sigma values at RS constants -/
 721
 722/-- σ_0(8) = 4. -/
 723theorem sigma_zero_eight : sigma 0 8 = 4 := by native_decide
 724
 725/-- σ_0(45) = 6. -/
 726theorem sigma_zero_fortyfive : sigma 0 45 = 6 := by native_decide
 727
 728/-- σ_0(360) = 24. -/
 729theorem sigma_zero_threehundredsixty : sigma 0 360 = 24 := by native_decide
 730
 731/-- σ_1(8) = 15. -/
 732theorem sigma_one_eight : sigma 1 8 = 15 := by native_decide
 733
 734/-- σ_1(45) = 78. -/
 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. -/