OAI/NumberTheory/DirichletL/GaussSum/RamifiedTracePhase.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TraceLambdaPhase.eisLam_sq line 23
  2. theorem OAI.TraceLambdaPhase.exp_minus_four_pi_div_three line 27
  3. theorem OAI.TraceLambdaPhase.breveE_traceLambda_square line 48
  4. theorem OAI.ActualEisensteinCubic.traceLambda_ne_zero line 67
  5. theorem OAI.ActualEisensteinCubic.traceLambda_span_eq_lambda line 73
  6. theorem OAI.ActualEisensteinCubic.traceLambda_quotient_card line 78
  7. theorem OAI.ActualEisensteinCubic.traceLambda_quotient_maximal line 83
  8. def OAI.ActualEisensteinCubic.quadraticGammaTraceLambda line 88
  9. theorem OAI.ActualEisensteinCubic.quadraticGammaTraceLambda_eq_I line 96
  10. def OAI.PoissonFirstLocal.quotientUnitMask line 148
  11. theorem OAI.PoissonFirstLocal.quotientUnitMask_mul line 151
  12. def OAI.PoissonFirstLocal.oldFactorRing line 159
  13. def OAI.PoissonFirstLocal.newFactorRing line 166
  14. theorem OAI.PoissonFirstLocal.first_local_identity_ring line 170
  15. theorem OAI.PoissonFirstLocal.first_prime_product_identity_ring line 200
  16. def OAI.ActualEisensteinCubic.quadraticGammaNegTraceLambda line 245
  17. theorem OAI.ActualEisensteinCubic.quadraticGammaNegTraceLambda_eq_neg_I line 253
  18. def OAI.ActualEisensteinCubic.finiteSquarefreeRow line 323
  19. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_sixth_power line 328
  20. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_difference line 347
  21. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_difference_norm line 365
  22. theorem OAI.ActualEisensteinCubic.first_local_identity_canonicalSextic line 378
  23. theorem OAI.ActualEisensteinCubic.first_prime_product_canonicalSextic line 389
  24. theorem OAI.AnalyticBridge.first_poisson_y_ball_of_scale_identity line 411
  25. def OAI.ShortDraftCusp.cuspMatrix line 441
  26. def OAI.ShortDraftCusp.unramifiedH line 442
  27. def OAI.ShortDraftCusp.unramifiedHInv line 443
  28. theorem OAI.ShortDraftCusp.A3_principal_matrix line 445
  29. theorem OAI.ShortDraftCusp.A3_ramified_inverse line 450
  30. theorem OAI.ShortDraftCusp.A3_ramified_inverse_left line 455
  31. theorem OAI.ShortDraftCusp.A3_ramified_matrix line 460
  32. theorem OAI.ShortDraftCusp.A3_unramified_H line 465
  33. theorem OAI.ShortDraftCusp.A3_unramified_inverse_right line 469
  34. theorem OAI.ShortDraftCusp.A3_unramified_inverse_left line 474
  35. theorem OAI.ShortDraftCusp.A3_unramified_matrix line 479
  36. theorem OAI.ShortDraftCusp.A3_ramified_det_relation line 484
  37. theorem OAI.ShortDraftCusp.A3_ramified_reciprocity_congr line 492
  38. theorem OAI.ShortDraftCusp.A3_unramified_det_relation line 500
  39. theorem OAI.ShortDraftCusp.A3_unramified_inverse_congr line 504
  40. theorem OAI.ActualEisensteinCubic.breveE_quarter_trace line 514
  41. def OAI.ActualEisensteinCubic.breveGaussianFourTerms line 538
  42. theorem OAI.ActualEisensteinCubic.breveGaussianFourTerms_formula line 545