mathlib
a8410892 - feat (number_theory/zeta_function): define zeta (#19027)

Commit

2 years ago

feat (number_theory/zeta_function): define zeta (#19027) This PR defines the Riemann zeta function (as a function on the whole complex plane).

Author

loefflerd

Parents