sigma_zero_prime_pow

formal source

 512/-! ### Sigma at prime powers -/
 513
 514/-- σ_0(p^k) = k + 1 for prime p (number of divisors of p^k). -/
 515theorem sigma_zero_prime_pow {p k : ℕ} (hp : Prime p) : sigma 0 (p ^ k) = k + 1 := by
 516  have hp' : Nat.Prime p := (prime_iff p).1 hp
 517  simp only [sigma_zero_apply]
 518  rw [Nat.divisors_prime_pow hp' k]
 519  simp
 520
 521/-- Concrete sigma values at small prime powers. -/
 522theorem sigma_one_two_pow_one : sigma 1 (2 ^ 1) = 3 := by native_decide
 523theorem sigma_one_two_pow_two : sigma 1 (2 ^ 2) = 7 := by native_decide
 524theorem sigma_one_two_pow_three : sigma 1 (2 ^ 3) = 15 := by native_decide
 525theorem sigma_one_three_pow_one : sigma 1 (3 ^ 1) = 4 := by native_decide
 526theorem sigma_one_three_pow_two : sigma 1 (3 ^ 2) = 13 := by native_decide
 527theorem sigma_one_five_pow_one : sigma 1 (5 ^ 1) = 6 := by native_decide
 528
 529/-! ### Totient multiplicativity -/
 530
 531/-- Euler's totient function is multiplicative. -/
 532theorem totient_isMultiplicative :
 533    ∀ {m n : ℕ}, Nat.Coprime m n → totient (m * n) = totient m * totient n := by
 534  intro m n h
 535  exact totient_mul_of_coprime h
 536
 537/-! ### Divisors of prime powers -/
 538
 539/-- The divisors of p^k are exactly {p^0, p^1, ..., p^k}. -/
 540theorem divisors_prime_pow {p k : ℕ} (hp : Prime p) :
 541    (p ^ k).divisors = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective hp.one_lt⟩ := by
 542  have hp' : Nat.Prime p := (prime_iff p).1 hp
 543  exact Nat.divisors_prime_pow hp' k
 544
 545/-- The number of divisors of p^k is k + 1. -/