OAI/NumberTheory/Ostmann/ZeroDensity/RealCharacterPairZeroBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One zeta pole controls the two distinct real-character zero sums

  1. theorem OAI.Ostmann.exists_distinct_real_zero_sum_bound line 12