OAI/NumberTheory/DukePrimeDegree/Arithmetic/StarkUnconditional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Unconditional odd-degree exceptional-zero exclusion

Artin reciprocity supplies even ray characters for each cyclic fixed field in the normal-closure argument. The resulting zero exclusion is transported to arbitrary universes.

  1. lemma OAI.DukePrimeDegree.hasCyclicRayRealizations_unconditional line 21
  2. theorem OAI.DukePrimeDegree.exceptionalRealZeroExclusion_unconditional line 34

    Source documentation

    Stark's real-zero exclusion in the exact odd-degree form needed by prime-degree packets.

    theorem exceptionalRealZeroExclusion_unconditional (d : ℕ) (hodd : Odd (d + 1)) :
    ExceptionalRealZeroExclusion.{u} d :=
…