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

14. References

←Blueprint Summary Blueprint Bibliography→

14. References🔗

←Blueprint Summary Blueprint Bibliography→