OAI/NumberTheory/Ostmann/ZeroDensity/CompletedCharacterConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The completed functional equation with conjugation

  1. theorem OAI.Ostmann.gammaReal_conjugate line 13
  2. theorem OAI.Ostmann.character_even_inverse_iff line 25
  3. theorem OAI.Ostmann.PrimitiveComplexCharacter.gammaFactor_inverse_conj line 36
  4. theorem OAI.Ostmann.PrimitiveComplexCharacter.gammaInverse_inverse_conj line 47
  5. theorem OAI.Ostmann.PrimitiveComplexCharacter.completed_inverse_conj_right line 51
  6. theorem OAI.Ostmann.PrimitiveComplexCharacter.inverse_completed_eq_conjugate line 67
  7. theorem OAI.Ostmann.PrimitiveComplexCharacter.completed_logDeriv_self_reflection line 80