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

2. Characters of the cyclotomic Galois group

2.1.	The Galois group
2.2.	Dirichlet characters
2.3.	Even and odd characters

←1.6. Injectivity of the class-group map and the definition of h-minus 2.1. The Galois group→

2. Characters of the cyclotomic Galois group🔗

This chapter fixes the character-theoretic notation used later.

2.1. The Galois group
2.2. Dirichlet characters
2.3. Even and odd characters

←1.6. Injectivity of the class-group map and the definition of h-minus 2.1. The Galois group→