OAI/NumberTheory/SiegelZeros/Characters/IntegerCharacter.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_gaussSum_mul_inv line 14
  2. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_gaussSum_sq line 43
  3. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_gaussSum_ne_zero line 53
  4. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_gaussSum_integer_square line 62
  5. theorem OAI.SiegelZeros.WeightedTorusJets.factorsThrough_ringHomComp_iff line 75
  6. theorem OAI.SiegelZeros.WeightedTorusJets.conductor_ringHomComp line 88
  7. def OAI.SiegelZeros.WeightedTorusJets.integerCharacter line 97
  8. theorem OAI.SiegelZeros.WeightedTorusJets.integerCharacter_cast line 115
  9. theorem OAI.SiegelZeros.WeightedTorusJets.integerCharacter_ringHomComp line 120
  10. theorem OAI.SiegelZeros.WeightedTorusJets.integerCharacter_isPrimitive line 126
  11. theorem OAI.SiegelZeros.WeightedTorusJets.integerCharacter_isQuadratic line 134
  12. theorem OAI.SiegelZeros.WeightedTorusJets.cyclotomic_gaussSum_action line 144
  13. def OAI.SiegelZeros.WeightedTorusJets.characterField line 174
  14. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_finrank line 177
  15. theorem OAI.SiegelZeros.WeightedTorusJets.mem_characterField_fixingSubgroup line 183
  16. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_changeLevel line 199
  17. theorem OAI.SiegelZeros.WeightedTorusJets.mem_adjoin_fixingSubgroup_iff line 236
  18. theorem OAI.SiegelZeros.WeightedTorusJets.gaussSum_adjoin_eq_characterField line 245
  19. theorem OAI.SiegelZeros.WeightedTorusJets.exists_squarefree_generator line 269
  20. theorem OAI.SiegelZeros.WeightedTorusJets.not_isSquare_of_quadratic_adjoin line 298
  21. theorem OAI.SiegelZeros.WeightedTorusJets.exists_squarefree_characterField_generator line 318
  22. theorem OAI.SiegelZeros.WeightedTorusJets.galEquivZMod_arithFrob line 368
  23. theorem OAI.SiegelZeros.WeightedTorusJets.arithFrob_map_character_eigenvector line 391
  24. theorem OAI.SiegelZeros.WeightedTorusJets.exists_squarefree_generator_frobenius_sign line 408
  25. def OAI.SiegelZeros.WeightedTorusJets.cyclotomicDivisorField line 438
  26. theorem OAI.SiegelZeros.WeightedTorusJets.cyclotomicDivisorField_isCyclotomicExtension line 443
  27. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_eighth_root_difference_sq line 452