The divisor power sums at prime powers

• ArithmeticFunction.sigma_prime_pow_succ: the recurrence σ_j(p^{m+1}) = p^j σ_j(p^m) + 1.

theorem ArithmeticFunction.sigma_prime_pow_succ {j p : ℕ} (hp : Nat.Prime p) (m : ℕ) : (sigma j) (p ^ (m + 1)) = p ^ j * (sigma j) (p ^ m) + 1

The prime-power recurrence for the divisor power sum: σ_j(p^{m+1}) = p^j σ_j(p^m) + 1.