theorem proved term proof

`riemannZeta_ne_zero_re_gt_one`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  37theorem riemannZeta_ne_zero_re_gt_one {s : ℂ} (hs : 1 < s.re) :
  38    riemannZeta s ≠ 0 :=

Term-mode proof.

  39  riemannZeta_ne_zero_of_one_lt_re hs
  40
  41/-- Certificate for the proved boundary zero-free region. -/

From the project-wide theorem graph. These declarations reference this one in their body.

boundaryZeroFreeCert in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use