OAI/NumberTheory/DirichletL/GaussSum/QuadraticTrace.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.omega_sq_for_norm line 24
  2. theorem OAI.ActualEisensteinCubic.conjO_eval_coordinates line 29
  3. theorem OAI.ActualEisensteinCubic.coordinate_norm_eq_mul_conjO line 37
  4. theorem OAI.ActualEisensteinCubic.algebraNorm_eq_coordinate_norm line 53
  5. theorem OAI.ActualEisensteinCubic.qNat_eq_absNorm_span line 59
  6. theorem OAI.ActualEisensteinCubic.prime_sixth_row_approx_ideal_norm line 71
  7. theorem OAI.ActualEisensteinCubic.sixth_power_eq_implies_same_prime_ideal line 94
  8. theorem OAI.ActualEisensteinCubic.sixth_power_rows_injective line 109
  9. theorem OAI.ActualEisensteinCubic.rational_modulus_card line 126
  10. theorem OAI.ActualEisensteinCubic.mk_eval_congr_mod line 140
  11. def OAI.ActualEisensteinCubic.rationalCoordMap line 160
  12. theorem OAI.ActualEisensteinCubic.rationalCoordMap_surjective line 165
  13. def OAI.ActualEisensteinCubic.rationalCoordEquiv line 179
  14. theorem OAI.ActualEisensteinCubic.breveE_rational_trace line 193
  15. theorem OAI.ActualEisensteinCubic.eisEmbedding_eval line 217
  16. theorem OAI.ActualEisensteinCubic.rationalCoordEquiv_apply line 229
  17. theorem OAI.ActualEisensteinCubic.rational_quadratic_phase line 235
  18. theorem OAI.ActualEisensteinCubic.rational_quadratic_character_sum line 264
  19. def OAI.ActualEisensteinCubic.quadraticGammaRational line 299
  20. theorem OAI.ActualEisensteinCubic.quadraticGammaRational_eq_one line 308
  21. theorem OAI.ActualEisensteinCubic.breveGaussianFourTerms_rational_odd line 339
  22. theorem OAI.ActualEisensteinCubic.quadraticGammaRational_eq_fourTerms line 358
  23. theorem OAI.ActualEisensteinCubic.cubic_roots_reduce_injective line 368
  24. theorem OAI.ActualEisensteinCubic.cubicChar_omega line 379
  25. theorem OAI.ActualEisensteinCubic.cubicChar_omega_eq_one_of_card_mod_nine line 393
  26. theorem OAI.ActualEisensteinCubic.cubicChar_omega_eq_omega_of_card_mod_nine line 401
  27. theorem OAI.ActualEisensteinCubic.cubicChar_omega_eq_omega_sq_of_card_mod_nine line 413
  28. theorem OAI.ActualEisensteinCubic.cubicChar_omega_sq line 422
  29. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_one line 429
  30. theorem OAI.ActualEisensteinCubic.finite_actual_prime_extraction line 439
  31. theorem OAI.ActualEisensteinCubic.breveE_int_trace_div line 497
  32. theorem OAI.ActualEisensteinCubic.breveE_quadratic_coordinate line 515
  33. theorem OAI.ActualEisensteinCubic.cubicChar_traceLambda_relation line 559
  34. theorem OAI.ActualEisensteinCubic.cubicChar_lambda_eq_one_sub_omega line 575
  35. theorem OAI.ActualEisensteinCubic.cubicChar_traceLambda_eq_lambda_of_card_mod_nine line 589