OAI/NumberTheory/SiegelZeros/Characters/CharacterLegendre.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.SiegelZerosAwei.W09.IsRealCharacter line 18
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.realCharacter_isQuadratic line 22
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.isQuadratic_isRealCharacter line 35
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.realCharacter_orderOf line 41
  5. def OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum line 45
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum_sq line 48
  7. def OAI.SiegelZeros.SiegelZerosAwei.W09.characterField line 62
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum_mem_field line 65
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum_ne_zero line 69
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum_isIntegral line 77
  11. def OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacterValue line 98
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacterValue_cast line 101
  13. def OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacter line 108
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacter_cast line 120
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacter_isQuadratic line 124
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.integerCharacter_complexification line 132
  17. def OAI.SiegelZeros.SiegelZerosAwei.W09.reducedIntegerCharacter line 138
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.reducedIntegerCharacter_isQuadratic line 142
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.reducedGaussSum_frobenius line 147
  20. theorem OAI.SiegelZeros.Awei.W39.character_legendre_of_reduced_gaussSum_sq line 164
  21. theorem OAI.SiegelZeros.Awei.W39.character_legendre_of_signed_gaussSum_sq line 177