have := sum_range_mul_zeta f N
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ range (N + 1), (N / d) • f d
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d