OAI/NumberTheory/DirichletL/GaussSum/FiniteFourier.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftFiniteGaussFourier.gauss_transform line 21
  2. theorem OAI.ShortDraftFiniteGaussFourier.product_gauss_transform line 35
  3. theorem OAI.PoissonChildCRT.inverse_as_row_and_label line 60
  4. theorem OAI.PoissonChildCRT.child_row_label_identity line 74
  5. def OAI.PoissonChildCRT.mask line 84
  6. theorem OAI.PoissonChildCRT.mask_mul line 86
  7. theorem OAI.PoissonChildCRT.mask_absorb_char line 105
  8. theorem OAI.PoissonChildCRT.mask_absorb_inv_char line 115
  9. theorem OAI.PoissonChildCRT.child_row_label_with_mask line 125
  10. theorem OAI.PoissonChildCRT.sum_child_row_label_with_mask line 153
  11. def OAI.PoissonFirstLocal.bit line 175
  12. def OAI.PoissonFirstLocal.localE line 176
  13. def OAI.PoissonFirstLocal.cExp₁ line 178
  14. def OAI.PoissonFirstLocal.cExp₂ line 180
  15. def OAI.PoissonFirstLocal.EExp line 182
  16. def OAI.PoissonFirstLocal.retained line 184
  17. def OAI.PoissonFirstLocal.totalExp₁ line 185
  18. def OAI.PoissonFirstLocal.totalExp₂ line 187
  19. theorem OAI.PoissonFirstLocal.exponent_table line 190
  20. def OAI.PoissonFirstLocal.mask line 195
  21. theorem OAI.PoissonFirstLocal.mask_mul line 197
  22. def OAI.PoissonFirstLocal.oldFactor line 216
  23. def OAI.PoissonFirstLocal.newFactor line 223
  24. theorem OAI.PoissonFirstLocal.first_local_identity line 227
  25. theorem OAI.PoissonFirstLocal.char_prod_four line 259
  26. theorem OAI.PoissonFirstLocal.mask_prod line 269
  27. theorem OAI.PoissonFirstLocal.first_prime_product_identity line 278
  28. theorem OAI.PoissonFirstLocal.mask_redundant_overlap line 300
  29. theorem OAI.PoissonFirstLocal.first_prime_product_with_b0 line 321
  30. theorem OAI.PoissonFirstLocal.sum_first_prime_product_identity line 335
  31. theorem OAI.PoissonFirstLocal.sum_first_prime_product_with_b0 line 349
  32. theorem OAI.ActualCubicChar.cubic_roots_surjective line 377
  33. def OAI.ActualCubicChar.cubic_roots_equiv line 391
  34. theorem OAI.ActualCubicChar.euler_jacobi_sum_zero line 406
  35. def OAI.ActualCubicChar.euler_to_roots line 429
  36. def OAI.ActualCubicChar.cubicResidueChar line 441
  37. theorem OAI.ActualCubicChar.cubicResidueChar_reduce_unit line 449
  38. theorem OAI.ActualCubicChar.cubicResidueChar_pow_three line 465
  39. abbrev OAI.ActualEisensteinCubic.K line 487
  40. abbrev OAI.ActualEisensteinCubic.O line 488
  41. instance OAI.ActualEisensteinCubic.(instance at line 490) line 490
  42. def OAI.ActualEisensteinCubic.omega line 493
  43. def OAI.ActualEisensteinCubic.lambda line 496
  44. instance OAI.ActualEisensteinCubic.quotientFintype line 498
  45. instance OAI.ActualEisensteinCubic.quotientField line 501
  46. theorem OAI.ActualEisensteinCubic.omega_primitive line 504
  47. def OAI.ActualEisensteinCubic.traceLambda line 507
  48. theorem OAI.ActualEisensteinCubic.traceLambda_eq_unit_mul_lambda line 509
  49. theorem OAI.ActualEisensteinCubic.neg_omega_isUnit line 517
  50. theorem OAI.ActualEisensteinCubic.traceLambda_mem_iff line 520
  51. theorem OAI.ActualEisensteinCubic.traceLambda_sq_dvd_iff line 524
  52. theorem OAI.ActualEisensteinCubic.omega_reduced_primitive line 529
  53. theorem OAI.ActualEisensteinCubic.card_sub_one_div_three line 553
  54. def OAI.ActualEisensteinCubic.cubicChar line 566
  55. theorem OAI.ActualEisensteinCubic.cubicChar_reduce line 578
  56. theorem OAI.ActualEisensteinCubic.cubicChar_pow_three line 608
  57. theorem OAI.ActualEisensteinCubic.cubicChar_ne_one line 623
  58. theorem OAI.ActualEisensteinCubic.cubicChar_order line 648
  59. theorem OAI.ActualEisensteinCubic.cubicJacobi_primary line 656
  60. theorem OAI.ActualEisensteinCubic.cubicJacobi_mem_prime line 670
  61. theorem OAI.ActualEisensteinCubic.cubicJacobi_product line 689
  62. def OAI.ActualEisensteinCubic.conjK line 726
  63. def OAI.ActualEisensteinCubic.conjO line 731
  64. theorem OAI.ActualEisensteinCubic.conjO_omega line 734
  65. theorem OAI.ActualEisensteinCubic.conjO_cubic_root line 742
  66. theorem OAI.ActualEisensteinCubic.cubicChar_conj_eq_inv line 749
  67. theorem OAI.ActualEisensteinCubic.cubicJacobi_conj line 767
  68. theorem OAI.ActualEisensteinCubic.cubicJacobi_mul_conj line 776
  69. def OAI.ActualEisensteinCubic.quadraticCharO line 786
  70. theorem OAI.ActualEisensteinCubic.quadraticCharO_sq line 793
  71. def OAI.ActualEisensteinCubic.sexticChar line 801
  72. theorem OAI.ActualEisensteinCubic.sexticChar_powers line 805
  73. theorem OAI.ActualEisensteinCubic.cubicJacobi_unit_multiple line 829
  74. theorem OAI.ActualEisensteinCubic.lambda_not_dvd_two line 852
  75. theorem OAI.ActualEisensteinCubic.cubicJacobi_eq_neg_primary_generator line 882
  76. theorem OAI.ActualEisensteinCubic.conjK_ne_refl line 914
  77. theorem OAI.ActualEisensteinCubic.galois_card_two line 932
  78. theorem OAI.ActualEisensteinCubic.galois_univ_pair line 940
  79. theorem OAI.ActualEisensteinCubic.norm_eq_mul_conjK line 947
  80. theorem OAI.ActualEisensteinCubic.norm_int_eq_mul_conjO line 955
  81. theorem OAI.ActualEisensteinCubic.generator_mul_conj_eq_sign_card line 963
  82. theorem OAI.ActualEisensteinCubic.cubicJacobi_unit_multiple_of_principal line 989
  83. theorem OAI.ActualEisensteinCubic.cubicJacobi_eq_neg_primary_generator_of_principal line 1030
  84. theorem OAI.ActualEisensteinCubic.cubicJacobi_generates_prime line 1061
  85. theorem OAI.ActualEisensteinCubic.cubicJacobi_exists_primary_generator line 1092
  86. theorem OAI.ActualEisensteinCubic.hgood_from_trace line 1106
  87. theorem OAI.ActualEisensteinCubic.cubicJacobi_eq_neg_primary_generator_trace line 1111
  88. theorem OAI.ActualEisensteinCubic.cubicGauss_cube line 1120
  89. def OAI.ActualEisensteinCubic.complexEmbedding line 1179
  90. def OAI.ActualEisensteinCubic.ringComplex line 1182
  91. theorem OAI.ActualEisensteinCubic.ringComplex_injective line 1185
  92. theorem OAI.ActualEisensteinCubic.ringComplex_conjO line 1188
  93. theorem OAI.ActualEisensteinCubic.cubicGauss_cube_complex line 1214
  94. theorem OAI.ActualEisensteinCubic.primary_generator_mul_conj_eq_card line 1225
  95. theorem OAI.ActualEisensteinCubic.cubicGauss_normalized_cube_complex line 1234
  96. theorem OAI.ActualEisensteinCubic.cubicGauss_cube_mulShift line 1261
  97. theorem OAI.ActualEisensteinCubic.quadraticCharO_ne_one line 1278
  98. theorem OAI.ActualEisensteinCubic.sexticChar_order line 1287
  99. theorem OAI.ActualEisensteinCubic.sexticChar_ne_quadratic_power line 1323
  100. theorem OAI.ActualEisensteinCubic.sexticChar_reduce_unit line 1337
  101. theorem OAI.ActualEisensteinCubic.quotient_char_ne_two_of_two_not_mem line 1384
  102. theorem OAI.ActualEisensteinCubic.sexticChar_zero_iff_mem line 1393
  103. theorem OAI.ActualEisensteinCubic.sexticChar_pow_zero_iff_mem line 1401