OAI/NumberTheory/DirichletL/Arithmetic/EisensteinEmbedding.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EisensteinEmbedding.K line 22
  2. abbrev OAI.EisensteinEmbedding.O line 23
  3. instance OAI.EisensteinEmbedding.(instance at line 25) line 25
  4. def OAI.EisensteinEmbedding.ζ line 28
  5. def OAI.EisensteinEmbedding.pb line 29
  6. def OAI.EisensteinEmbedding.omega3 line 32
  7. theorem OAI.EisensteinEmbedding.omega3_sq line 34
  8. theorem OAI.EisensteinEmbedding.omega3_im line 45
  9. theorem OAI.EisensteinEmbedding.omega3_im_ne_zero line 48
  10. theorem OAI.EisensteinEmbedding.lam_ne_zero line 52
  11. theorem OAI.EisensteinEmbedding.pb_minpoly line 59
  12. def OAI.EisensteinEmbedding.embedding line 75
  13. theorem OAI.EisensteinEmbedding.embedding_gen line 80
  14. theorem OAI.EisensteinEmbedding.pb_dim line 86
  15. theorem OAI.EisensteinEmbedding.exists_ab line 92
  16. theorem OAI.EisensteinEmbedding.embedding_apply_ab line 110
  17. theorem OAI.EisensteinEmbedding.embedding_injective line 116
  18. theorem OAI.EisensteinEmbedding.trace_period_on_ringOfIntegers line 136
  19. def OAI.ConcreteTraceCRT.eisEmbedding line 153
  20. theorem OAI.ConcreteTraceCRT.eisEmbedding_injective line 155
  21. theorem OAI.ConcreteTraceCRT.eisEmbedding_ne_zero line 158
  22. def OAI.ConcreteTraceCRT.eisLam line 162
  23. theorem OAI.ConcreteTraceCRT.eisLam_ne_zero line 164
  24. theorem OAI.ConcreteTraceCRT.eisPeriod line 166
  25. def OAI.ConcreteTraceCRT.coordinateSubring line 172
  26. theorem OAI.ConcreteTraceCRT.coordinateSubring_eq_traceSubring line 192
  27. def OAI.ConcreteTraceCRT.toCoordinateSubring line 196
  28. theorem OAI.ConcreteTraceCRT.toCoordinateSubring_injective line 205
  29. theorem OAI.ConcreteTraceCRT.toCoordinateSubring_surjective line 210
  30. def OAI.ConcreteTraceCRT.ringOfIntegersEquivCoordinateSubring line 219
  31. def OAI.ConcreteTraceCRT.eisTraceModChar line 223
  32. def OAI.ConcreteTraceCRT.eisTraceProdChar line 231
  33. theorem OAI.ConcreteTraceCRT.gauss_sum_actual_O line 241
  34. theorem OAI.ConcreteTraceCRT.finite_quotient_span line 267
  35. theorem OAI.ConcreteTraceCRT.finite_quotient_product line 273
  36. theorem OAI.ConcreteBreveE.breveE_period_coordinates line 287
  37. theorem OAI.ConcreteBreveE.coordinateSubring_eq line 297
  38. def OAI.ConcreteBreveE.ringOfIntegersEquivShortDraftE line 301
  39. theorem OAI.ConcreteBreveE.gauss_sum_breveE_actual_O line 305
  40. theorem OAI.ActualEisensteinCubic.eisEmbedding_conjO line 333
  41. theorem OAI.ActualEisensteinCubic.cubicGauss_normalized_cube_eis line 361
  42. theorem OAI.ActualEisensteinCubic.sextic_complex_pow_ne_one line 392
  43. theorem OAI.ActualEisensteinCubic.sextic_local_fourier_nonzero line 401
  44. theorem OAI.ActualEisensteinCubic.sextic_local_fourier_zero line 419
  45. theorem OAI.ActualEisensteinCubic.sextic_local_fourier_jzero_nonzero line 432
  46. theorem OAI.ActualEisensteinCubic.sextic_local_fourier_jzero_zero line 445
  47. def OAI.ActualEisensteinCubic.canonicalSextic line 461
  48. theorem OAI.ActualEisensteinCubic.canonicalSextic_pow_six line 465
  49. theorem OAI.ActualEisensteinCubic.canonicalSextic_pow_ne_one line 471
  50. theorem OAI.ActualEisensteinCubic.canonical_A5_jone line 482
  51. theorem OAI.ActualEisensteinCubic.canonical_A5_jfour line 504
  52. theorem OAI.ActualEisensteinCubic.canonical_A5_jzero_active line 544
  53. theorem OAI.PrimitiveTrace.complex_exp_trace_integer line 590
  54. theorem OAI.PrimitiveTrace.phase_integer line 603
  55. theorem OAI.PrimitiveTrace.omega_conj line 609
  56. theorem OAI.PrimitiveTrace.reconstruction line 618
  57. theorem OAI.PrimitiveTrace.in_coordinate_lattice_of_two_phases line 632
  58. theorem OAI.PrimitiveTrace.eisTraceModChar_breveE_ne_one line 649
  59. theorem OAI.PrimitiveTrace.eisTraceModChar_breveE_primitive line 687