OAI/NumberTheory/DirichletL/Hecke/Nonvanishing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-order Hecke L-functions over the Eisenstein number field are nonzero to the right of seven eighths, away from the principal pole.

  1. theorem OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_seven_eighths_lt_re line 13

    Distinct definitions of this name: ComparatorChallenges/HeckeSevenEighths.lean:237 (same statement text; different proof or body). Qualify references as OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_seven_eighths_lt_re@path.

  2. theorem OAI.SevenEighths.HeckeFamily.LFunction_ofResidue_ne_zero_of_seven_eighths_lt_re line 19
  3. theorem OAI.SevenEighths.HeckeRayFamily.LFunction_ne_zero_of_seven_eighths_lt_re line 35