Library
SawinTotallyRealTowers
A Lean 4 proof of Sawin's totally real tower theorem. One infinite set of primes congruent to 1 modulo 4 splits completely in totally real number fields of arbitrarily large degree with a uniform root discriminant bound.
Repository: https://github.com/n-yamaguchi-0729/SawinTotallyRealTowers
Formalized results
- Sawin's totally real tower theorem, with the prime set fixed before every degree bound.
- Infinitely many completely split primes congruent to 1 modulo 4.
- Totally real number fields of arbitrarily large degree.
- A uniform root discriminant bound of 255255.