mathlib3

cca40788 - feat (number_theory/zeta_function): relate to Dirichlet series (#19131)

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.