sigma_zero_apply

formal source

 179  simp only [sigma, ArithmeticFunction.sigma_apply]
 180
 181/-- σ_0(n) = number of divisors of n. -/
 182theorem sigma_zero_apply {n : ℕ} : sigma 0 n = n.divisors.card := by
 183  simp only [sigma, ArithmeticFunction.sigma_zero_apply]
 184
 185/-- σ_1(n) = sum of divisors of n. -/
 186theorem sigma_one_apply {n : ℕ} : sigma 1 n = ∑ d ∈ n.divisors, d := by
 187  simp only [sigma, ArithmeticFunction.sigma_one_apply]
 188
 189/-- σ_k is multiplicative. -/
 190theorem sigma_isMultiplicative (k : ℕ) : ArithmeticFunction.IsMultiplicative (sigma k) := by
 191  simp only [sigma]
 192  exact ArithmeticFunction.isMultiplicative_sigma
 193
 194/-- σ_0(p) = 2 for prime p. -/
 195theorem sigma_zero_prime {p : ℕ} (hp : Prime p) : sigma 0 p = 2 := by
 196  have hp' : Nat.Prime p := (prime_iff p).1 hp
 197  simp only [sigma_zero_apply, hp'.divisors]
 198  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 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