1 Characters and Bernoulli factors
Dirichlet characters modulo \(p\) are used as the character side of the cyclotomic zeta factorisation and of the Teichmuller congruence.
For a Dirichlet character \(\chi \), the generalized Bernoulli number is denoted
The final class-number formula only needs the values \(B_{1,\chi ^{-1}}\) for odd characters.
For a prime \(p\), the Teichmuller character valued in \(\mathbb {Q}_p\) is written
For \(0{\lt}n{\lt}p-1\), the classical Bernoulli number \(B_n\) is \(p\)-adically integral.
The proof uses the von Staudt–Clausen denominator description: the only possible prime divisors of the denominator of \(B_n\) are primes \(q\) with \(q-1\mid n\). Since \(n{\lt}p-1\), the prime \(p\) cannot occur.
For \(0{\lt}n{\lt}p-1\), the prime \(p\) does not divide the denominator of \(B_n\).
This is the denominator form of theorem 1.4. Lean passes between \(p\)-adic integrality and the rational denominator condition.
For \(0{\lt}n{\lt}p-1\), the factor \(B_n/n\) has a representative in \(\mathbb {Z}_p\), and that representative is a \(p\)-adic unit exactly when \(p\) does not divide the numerator of \(B_n\).
The denominator is prime to \(p\) by theorem 1.5, so the rational number \(B_n/n\) lies in \(\mathbb {Z}_p\). In \(\mathbb {Z}_p\), non-units are precisely the elements with norm \({\lt}1\), equivalently elements divisible by \(p\); this is translated back to divisibility of the Bernoulli numerator.
For the odd Teichmuller powers used in the relative class-number formula,
This is the bridge from generalized Bernoulli values to classical Bernoulli numbers. The proof uses the Kummer congruence machinery and checks the range hypotheses ensuring that \(j+1\) is neither divisible by \(p\) nor by \(p-1\).