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
11.
Fermat's Last Theorem for exponent 37
11.1.
Background: irregular primes and Vandiver's Theorem III
11.2.
The case-decomposition
11.3.
Case I: the Mirimanoff route
11.4.
Case II: descent under 37 not dividing h-plus
11.5.
Assembly
11.6.
Supporting machinery developed in the project
11.7.
Outlook
←
10.5. How the reciprocity input is to be proved
11.1. Background: irregular primes and Vandiver's Theorem III
→
11. Fermat's Last Theorem for exponent 37
🔗
11.1.
Background: irregular primes and Vandiver's Theorem III
11.2.
The case-decomposition
11.3.
Case I: the Mirimanoff route
11.4.
Case II: descent under 37 not dividing h-plus
11.5.
Assembly
11.6.
Supporting machinery developed in the project
11.7.
Outlook
←
10.5. How the reciprocity input is to be proved
11.1. Background: irregular primes and Vandiver's Theorem III
→