simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : 1 < s.re
hs₁ : s ≠ 1
⊢ (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
no goals