546theorem analyticAt_riemannZeta {s : ℂ} (hs : s ≠ 1) : 547 AnalyticAt ℂ riemannZeta s := by
proof body
Term-mode proof.
548 have hdiff : DifferentiableOn ℂ riemannZeta {(1 : ℂ)}ᶜ := 549 fun z hz => (differentiableAt_riemannZeta hz).differentiableWithinAt 550 exact hdiff.analyticAt (isOpen_compl_singleton.mem_nhds hs) 551 552/-- `zetaReciprocal` is meromorphic at every point of the strip (away from `s=1`). 553This follows from `riemannZeta` being analytic at `s ≠ 1` and the inverse 554of a meromorphic function being meromorphic. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.