OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterNonrealZeros.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Characters whose square is nonprincipal have a classical zero-free strip at every height. The real quadratic exceptional-zero case is excluded explicitly by the square-character hypothesis.

  1. theorem OAI.TwoPointCorrelations.mrt_character_nonreal_zero_free line 14