OAI/NumberTheory/DukePrimeDegree/Arithmetic/StarkNormalClosure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Assembling the normal-closure argument

Realizing cyclic Frobenius characters by even ray characters gives zero propagation to the normal closure. Simplicity near one and odd-index descent then exclude an exceptional real zero.

  1. lemma OAI.DukePrimeDegree.fixedFieldMultiplicity_fixingSubgroup line 24
  2. lemma OAI.DukePrimeDegree.fixingSubgroup_index_of_embedding line 35
  3. theorem OAI.DukePrimeDegree.exceptionalRealZeroExclusion_of_ray_realizations line 44

    Source documentation

    The zero-exclusion consequence of cyclic reciprocity, for the exact family of normal closures required by the application.

    theorem exceptionalRealZeroExclusion_of_ray_realizations
    (d : ℕ) (hodd : Odd (d + 1))
    (hray : ∀ (E : Type u) [Field E] [NumberField E] [IsGalois ℚ E]
      [NumberField.IsTotallyReal E], HasCyclicRayRealizations E) :
    ExceptionalRealZeroExclusion.{u} d := by
…

    Mentions: OAI.DukePrimeDegree.HasCyclicRayRealizations