OAI/NumberTheory/Ostmann/ZeroDensity/RealCharacterConjugateZeros.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Conjugate partners in the actual real-character zero family

  1. theorem OAI.Ostmann.PrimitiveRealCharacter.L_conj_right line 14
  2. theorem OAI.Ostmann.PrimitiveRealCharacter.L_conj line 35
  3. theorem OAI.Ostmann.actualCharacterZeros_complete line 54
  4. theorem OAI.Ostmann.realCharacterActualZeros_conjugate line 64