Kummer's Criterion and Regular Primes in Lean

3. Generalised Bernoulli numbers🔗

This chapter introduces the generalised Bernoulli numbers B_{n,\chi} attached to a Dirichlet character \chi and records the properties of these numbers needed for the analytic formula for \hminus.

  1. 3.1. Definition
  2. 3.2. Vanishing in degree 0
  3. 3.3. The first generalised Bernoulli number
  4. 3.4. Congruences with classical Bernoulli numbers