OAI/NumberTheory/DirichletL/Eisenstein/SourceProjection.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.finite_tsum_comp_addHom line 84
  2. lemma OAI.CubicEisenstein.ramified_affine_isUnit line 96
  3. def OAI.CubicEisenstein.ramifiedAffineEquiv line 104
  4. theorem OAI.CubicEisenstein.ramified_arithmetic_affine line 108
  5. def OAI.CubicEisenstein.ramifiedReduction line 128
  6. lemma OAI.CubicEisenstein.ramifiedReduction_surjective line 133
  7. lemma OAI.CubicEisenstein.ramifiedReduction_rep line 137
  8. lemma OAI.CubicEisenstein.residueAdditive_ramified_scale line 148
  9. def OAI.CubicEisenstein.ramifiedNineSum line 159
  10. lemma OAI.CubicEisenstein.ramifiedReduction_kernel_card line 165
  11. theorem OAI.CubicEisenstein.ramified_arithmetic_nine_sum line 179
  12. def OAI.CubicEisenstein.ramifiedLinearChar line 216
  13. lemma OAI.CubicEisenstein.ramifiedLinearChar_period line 227
  14. def OAI.CubicEisenstein.ramifiedQuotientChar line 234
  15. lemma OAI.CubicEisenstein.ramifiedQuotientChar_rep line 237
  16. def OAI.CubicEisenstein.ramifiedFrequencyChar line 244
  17. lemma OAI.CubicEisenstein.ramifiedFrequencyChar_rep line 250
  18. theorem OAI.CubicEisenstein.ramifiedNineSum_eq_character_test line 265
  19. theorem OAI.CubicEisenstein.ramified_arithmetic_character_test line 288
  20. def OAI.CubicKubota.levelThreeInTwo line 314
  21. instance OAI.CubicKubota.levelThreeInTwo_normal line 316
  22. instance OAI.CubicKubota.levelThreeInTwo_finiteIndex line 321
  23. def OAI.CubicKubota.rationalLift line 326
  24. def OAI.CubicKubota.rationalQuotient line 331
  25. theorem OAI.CubicKubota.rationalQuotient_surjective line 334
  26. def OAI.CubicKubota.rationalCongruenceThree line 346
  27. instance OAI.CubicKubota.rationalCongruenceThree_normal line 348
  28. theorem OAI.CubicKubota.mem_rationalCongruenceThree line 352
  29. def OAI.CubicKubota.rationalQuotientEquiv line 357
  30. instance OAI.CubicKubota.rationalCongruenceThree_finiteIndex line 361
  31. theorem OAI.CubicKubota.finite_rational_representatives line 369
  32. lemma OAI.CubicKubota.three_dvd_intCast_iff line 390
  33. lemma OAI.CubicKubota.mem_levelThree_iff_entries line 405
  34. def OAI.CubicKubota.rationalReductionThree line 422
  35. lemma OAI.CubicKubota.rationalReductionThree_eq_one_iff line 425
  36. abbrev OAI.CubicKubota.RationalBruhatIndex line 454
  37. def OAI.CubicKubota.rationalBruhatRep line 456
  38. lemma OAI.CubicKubota.rationalBruhat_complete line 461
  39. lemma OAI.CubicKubota.rationalReductionThree_surjective line 465
  40. lemma OAI.CubicKubota.rationalBruhat_injective line 470
  41. def OAI.CubicKubota.rationalBruhatEquiv line 474
  42. lemma OAI.CubicKubota.card_SLThree line 478
  43. lemma OAI.CubicKubota.rationalCongruenceThree_eq_ker line 482
  44. def OAI.CubicKubota.rationalCongruenceEquivSLThree line 486
  45. def OAI.CubicKubota.sourceQuotientEquivSLThree line 490
  46. lemma OAI.CubicKubota.sourceQuotient_card line 493
  47. lemma OAI.CubicKubota.levelThreeInTwo_index line 496
  48. theorem OAI.CubicKubota.twentyFour_rational_representatives line 498
  49. lemma OAI.CubicKubota.rationalQuotient_eq_iff_reduction line 525
  50. lemma OAI.CubicKubota.levelTwoComplexCharacter_rationalLift line 533
  51. def OAI.CubicKubota.rationalCosetEquiv line 536
  52. instance OAI.CubicKubota.sourceQuotientFintype line 545
  53. def OAI.CubicKubota.sourceRationalSection line 547
  54. lemma OAI.CubicKubota.sourceRationalSection_spec line 550
  55. def OAI.CubicKubota.sourceProjection line 553
  56. lemma OAI.CubicKubota.sourceProjection_eq_twentyFour line 557
  57. lemma OAI.CubicKubota.sourceSection_translate line 565
  58. theorem OAI.CubicKubota.sourceProjection_automorphy line 599
  59. theorem OAI.CubicKubota.sourceProjection_fixed line 612
  60. lemma OAI.CubicKubota.sourceProjection_idempotent line 629
  61. def OAI.CubicKubota.sourceEisenstein line 635
  62. theorem OAI.CubicKubota.sourceEisenstein_automorphy line 637