Commit 2023-06-07 07:55 81843c08

View on Github →

feat (number_theory/zeta_function): func eqn + link to Bernoulli nos (#19158) Functional equation relating zeta (1 - s) to zeta s, and formula for zeta (-k) for nat k in terms of Bernoulli numbers.

Estimated changes

Modified src/number_theory/zeta_function.lean

added theorem riemann_completed_zeta_one_sub

added theorem riemann_completed_zeta₀_one_sub

added theorem riemann_zeta_four

added theorem riemann_zeta_neg_nat_eq_bernoulli

added theorem riemann_zeta_one_sub

added theorem riemann_zeta_two

added theorem riemann_zeta_two_mul_nat

deleted theorem zeta_eq_tsum_of_one_lt_re

added theorem zeta_eq_tsum_one_div_nat_add_one_cpow

added theorem zeta_eq_tsum_one_div_nat_cpow

added theorem zeta_nat_eq_tsum_of_gt_one