ClassFieldTower.Sawin.sawin_totally_real_tower
Sawin's totally real tower, with one prime set fixed before the degree bound.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open AlgebraicNumberTheory.PrimeSelection
open AlgebraicNumberTheory.DiscriminantBoundsLean source · statement
theorem sawin_totally_real_tower :
∃ (rdBound : ℝ) (Q : Set ℕ), Q.Infinite ∧ (∀ q ∈ Q, q.Prime ∧ q % 4 = 1) ∧
∀ N : ℕ, ∃ (F : Type) (_ : Field F) (_ : CharZero F) (_ : NumberField F)
(_ : IsTotallyReal F),
N ≤ Module.finrank ℚ F ∧
(|(NumberField.discr F : ℝ)|) ^ ((1 : ℝ) / Module.finrank ℚ F) ≤ rdBound ∧
∀ q ∈ Q, ∃ (factors : Finset (Ideal (𝓞 F))),
factors.card = Module.finrank ℚ F ∧
∀ p ∈ factors, p.IsMaximal ∧ (q : 𝓞 F) ∈ p