Kummer's Criterion and Regular Primes in Lean

Kummer's Criterion and Regular Primes in Lean

Table of Contents

1.	The CM field and the class number splitting
2.	Characters of the cyclotomic Galois group
3.	Generalised Bernoulli numbers
4.	Gauss sums and Stickelberger
5.	L-values at non-positive integers
6.	The relative class number h-minus
7.	Cyclotomic units and the plus class number
8.	The final proof of Kummer's criterion
9.	Infinitely many irregular primes
10.	The abandoned reflection route
11.	Fermat's Last Theorem for exponent 37
12.	Dependency graph
	Dependency Graph
13.	Progress summary
	Blueprint Summary
14.	References
	Blueprint Bibliography

5. L-values at non-positive integers

5.1.	The value at s = 0
5.2.	The value at s = 1

←4.3. Herbrand's theorem 5.1. The value at s = 0→

5. L-values at non-positive integers🔗

This chapter records the special values of Dirichlet L-functions needed for the analytic formula for \hminus.

5.1. The value at s = 0
5.2. The value at s = 1

←4.3. Herbrand's theorem 5.1. The value at s = 0→