OAI/NumberTheory/Jacobsthal/Siegel/IntegerCharacter.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.primitive_gaussSum_mul_inv line 14
  2. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_gaussSum_sq line 43
  3. theorem OAI.Erdos970.WeightedTorusJets.primitive_gaussSum_ne_zero line 53
  4. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_gaussSum_integer_square line 62
  5. theorem OAI.Erdos970.WeightedTorusJets.factorsThrough_ringHomComp_iff line 77
  6. theorem OAI.Erdos970.WeightedTorusJets.conductor_ringHomComp line 90
  7. def OAI.Erdos970.WeightedTorusJets.integerCharacter line 99
  8. theorem OAI.Erdos970.WeightedTorusJets.integerCharacter_cast line 117
  9. theorem OAI.Erdos970.WeightedTorusJets.integerCharacter_ringHomComp line 122
  10. theorem OAI.Erdos970.WeightedTorusJets.integerCharacter_isPrimitive line 128
  11. theorem OAI.Erdos970.WeightedTorusJets.integerCharacter_isQuadratic line 136
  12. theorem OAI.Erdos970.WeightedTorusJets.cyclotomic_gaussSum_action line 148
  13. def OAI.Erdos970.WeightedTorusJets.characterField line 180
  14. theorem OAI.Erdos970.WeightedTorusJets.characterField_finrank line 183
  15. theorem OAI.Erdos970.WeightedTorusJets.mem_characterField_fixingSubgroup line 189
  16. theorem OAI.Erdos970.WeightedTorusJets.characterField_changeLevel line 205
  17. theorem OAI.Erdos970.WeightedTorusJets.mem_adjoin_fixingSubgroup_iff line 242
  18. theorem OAI.Erdos970.WeightedTorusJets.gaussSum_adjoin_eq_characterField line 251
  19. theorem OAI.Erdos970.WeightedTorusJets.exists_squarefree_generator line 277
  20. theorem OAI.Erdos970.WeightedTorusJets.not_isSquare_of_quadratic_adjoin line 308
  21. theorem OAI.Erdos970.WeightedTorusJets.exists_squarefree_characterField_generator line 328
  22. theorem OAI.Erdos970.WeightedTorusJets.galEquivZMod_arithFrob line 380
  23. theorem OAI.Erdos970.WeightedTorusJets.arithFrob_map_character_eigenvector line 403
  24. theorem OAI.Erdos970.WeightedTorusJets.exists_squarefree_generator_frobenius_sign line 426
  25. def OAI.Erdos970.WeightedTorusJets.cyclotomicDivisorField line 456
  26. theorem OAI.Erdos970.WeightedTorusJets.cyclotomicDivisorField_isCyclotomicExtension line 461
  27. theorem OAI.Erdos970.WeightedTorusJets.primitive_eighth_root_difference_sq line 472