case h
n : ℕ
⊢ ↑(Λ * ↑ζ) n = ↑log n
⊢ Λ * ↑ζ = log
ext n
case h
n : ℕ
⊢ Real.log ↑n = ↑log n
case h
n : ℕ
⊢ ↑(Λ * ↑ζ) n = ↑log n
rw [coe_mul_zeta_apply, vonMangoldt_sum]
no goals
case h
n : ℕ
⊢ Real.log ↑n = ↑log n
rfl