Millennium · test · AMS 11

easyknown result, no worker yet

Riemann Hypothesis and its generalizations

Exercise · implies_riemannHypothesis

GRH for χ=1\chi = 1 is RiemannHypothesis.

Formal statement · Lean 4.lean
theorem implies_riemannHypothesis :
    type_of% (generalized_riemann_hypothesis 1 1) ↔ RiemannHypothesis := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗