Commit 2023-05-31 19:23 cca40788

feat (number_theory/zeta_function): relate to Dirichlet series (#19131) This PR adds two important properties of the Riemann zeta function: firstly, it is differentiable away from s = 1 (which is easy for s ≠ 0, but much harder at s = 0); secondly, for 1 < re s the zeta function is given by the usual Dirichlet series. Just for fun, we also add a formal statement of the Riemann hypothesis.