OAI/NumberTheory/DukePrimeDegree/Arithmetic/FieldDegree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Prime degree excludes quadratic subfields

The tower-degree formula excludes the quadratic subfields in Stark's exceptional-zero alternative, giving the field-degree hypothesis for the uniform residue estimate.

  1. theorem OAI.DukePrimeDegree.no_quadratic_intermediateField line 18

    Source documentation

    A number field of prime degree at least three has no quadratic intermediate field over the rationals.

    theorem no_quadratic_intermediateField
    {K : Type*} [Field K] [NumberField K]
    (hprime : (Module.finrank ℚ K).Prime) (hdegree : 3 ≤ Module.finrank ℚ K)
    (F : IntermediateField ℚ K) : Module.finrank ℚ F ≠ 2 := by
…