NYLL
Module

SawinDiscriminantBound.lean

Nyll.SawinTotallyRealTowers.SawinDiscriminantBound
1 declaration indexed from sourceView source ↗

Module documentation

A uniform discriminant bound for the initial Sawin tower

The degree of every finite admissible layer is a power of two. Its ramified rational primes belong to {3,5,7,11,13,17}, whose product is

  1. The prime-to-degree different bound gives the same root scale

255255 for every such finite Galois layer.

Imports6
Imported by2

Declarations

theorem

discr_natAbs_le_of_sawin_ramification

L32 ↗
ClassFieldTower.Sawin.discr_natAbs_le_of_sawin_ramification
Documentation

The initial tower's arithmetic conditions give a discriminant bound with one constant for all finite Galois number fields satisfying them.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
theorem discr_natAbs_le_of_sawin_ramification
    (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]
    (hP : IsPGroup 2 Gal(L/ℚ))
    (hOutside : IsUnramifiedAtFinitePlacesOutside ℚ L sawinRationalPrimeSupport) :
    (NumberField.discr L).natAbs ≤ 255255 ^ Module.finrank ℚ L

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.