sigma_one_prime

formal source

 199  rw [Finset.card_insert_of_notMem (by simp [h_ne]), Finset.card_singleton]
 200
 201/-- σ_1(p) = p + 1 for prime p. -/
 202theorem sigma_one_prime {p : ℕ} (hp : Prime p) : sigma 1 p = p + 1 := by
 203  have hp' : Nat.Prime p := (prime_iff p).1 hp
 204  simp only [sigma_one_apply, hp'.divisors]
 205  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 206  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, add_comm]
 207
 208/-- σ_k(p) = 1 + p^k for prime p. -/
 209theorem sigma_prime {k : ℕ} {p : ℕ} (hp : Prime p) : sigma k p = 1 + p ^ k := by
 210  have hp' : Nat.Prime p := (prime_iff p).1 hp
 211  simp only [sigma_apply, hp'.divisors]
 212  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 213  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, one_pow, add_comm]
 214
 215/-! ### Zeta function (constant 1) and Dirichlet convolution -/
 216
 217/-- The arithmetic zeta function ζ (constant 1 on positive integers). -/
 218abbrev zeta : ArithmeticFunction ℕ := ArithmeticFunction.zeta
 219
 220@[simp] theorem zeta_def : zeta = ArithmeticFunction.zeta := rfl
 221
 222/-- ζ(n) = 1 for n ≥ 1. -/
 223theorem zeta_apply {n : ℕ} (hn : n ≠ 0) : zeta n = 1 := by
 224  simp only [zeta, ArithmeticFunction.zeta_apply, hn, ↓reduceIte]
 225
 226/-- ζ(0) = 0. -/
 227theorem zeta_zero : zeta 0 = 0 := by
 228  simp only [zeta, ArithmeticFunction.zeta_apply, ↓reduceIte]
 229
 230/-- ζ is multiplicative. -/
 231theorem zeta_isMultiplicative : ArithmeticFunction.IsMultiplicative zeta := by
 232  simp only [zeta]