Kummer's Criterion and Regular Primes in Lean

4. Gauss sums and Stickelberger🔗

This chapter assembles the algebraic ingredients that give the Herbrand implication: a non-trivial \chi-eigenspace in the p-part of the class group forces p \mid B_{1,\chi}. The analytic chapters below use the same Gauss-sum normalization in the relative class-number formula.

  1. 4.1. Gauss sums
  2. 4.2. The Stickelberger element
  3. 4.3. Herbrand's theorem