OAI/NumberTheory/SiegelZeros/Structure/GaussFixedField.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.exists_unit_apply_neg_one line 18
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.quadratic_unitHom_range line 28
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.quadratic_kernel_index line 52
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.actualCyclotomicField_isCyclotomic line 58
  5. def OAI.SiegelZeros.SiegelZerosAwei.W09.cyclotomicGaloisEquiv line 63
  6. def OAI.SiegelZeros.SiegelZerosAwei.W09.cyclotomicCharacter line 69
  7. def OAI.SiegelZeros.SiegelZerosAwei.W09.quadraticFixedField line 73
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.cyclotomicCharacter_kernel_index line 77
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.quadraticFixedField_finrank line 91
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterField_finiteDimensional line 113
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.finrank_adjoin_le_two_of_sq_eq_rat line 119
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterField_finrank_le_two line 131
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterGaussSum_norm_sq line 140
  14. def OAI.SiegelZeros.SiegelZerosAwei.W09.standardRoot line 156
  15. def OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicField line 159
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.standardRoot_isPrimitive line 162
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.standardAddChar_eq_pow line 169
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.standardAddChar_mem line 174
  19. def OAI.SiegelZeros.SiegelZerosAwei.W09.liftedAddChar line 181
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.quadraticCharacterValue_mem line 184
  21. def OAI.SiegelZeros.SiegelZerosAwei.W09.liftedCharacterValue line 191
  22. def OAI.SiegelZeros.SiegelZerosAwei.W09.liftedGaussSum line 195
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.coe_liftedGaussSum line 199
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.standardRoot_lift_isPrimitive line 204
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicField_isCyclotomic line 209
  26. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.automorphism_liftedCharacterValue line 218
  27. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.automorphism_liftedAddChar line 230
  28. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.automorphism_liftedGaussSum line 245
  29. def OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicGaloisEquiv line 259
  30. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicGaloisEquiv_apply line 278
  31. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicGaloisEquiv_spec line 283
  32. def OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicCharacter line 292
  33. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.gaussSum_galois_action line 296
  34. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.fixes_gaussSum_iff_kernel line 304
  35. def OAI.SiegelZeros.SiegelZerosAwei.W09.liftedGaussField line 323
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.liftedGaussField_fixingSubgroup line 327
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.liftedGaussField_eq_fixedField line 347
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.liftedGaussField_map line 360
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterField_eq_fixedField_map line 367
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.complexCyclotomicCharacter_kernel_index line 374
  41. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.characterField_finrank line 388