OAI/NumberTheory/DirichletL/Cusp/ResiduesModThree.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EisensteinCuspModThree.Pair line 85
  2. def OAI.EisensteinCuspModThree.add line 86
  3. def OAI.EisensteinCuspModThree.neg line 87
  4. def OAI.EisensteinCuspModThree.sub line 88
  5. def OAI.EisensteinCuspModThree.mul line 89
  6. def OAI.EisensteinCuspModThree.scalar line 90
  7. def OAI.EisensteinCuspModThree.residue line 91
  8. lemma OAI.EisensteinCuspModThree.residue_eval line 93
  9. lemma OAI.EisensteinCuspModThree.residue_intCast line 98
  10. lemma OAI.EisensteinCuspModThree.residue_zero line 101
  11. lemma OAI.EisensteinCuspModThree.residue_one line 102
  12. lemma OAI.EisensteinCuspModThree.residue_add line 104
  13. lemma OAI.EisensteinCuspModThree.residue_neg line 112
  14. lemma OAI.EisensteinCuspModThree.residue_sub line 120
  15. lemma OAI.EisensteinCuspModThree.residue_mul line 124
  16. lemma OAI.EisensteinCuspModThree.residue_eq_implies_three_dvd line 130
  17. lemma OAI.EisensteinCuspModThree.residue_mul_intCast line 147
  18. def OAI.EisensteinCuspModThree.primitive line 151
  19. instance OAI.EisensteinCuspModThree.primitive_decidable line 152
  20. lemma OAI.EisensteinCuspModThree.primitive_of_determinant line 155
  21. lemma OAI.EisensteinCuspModThree.first_column_primitive line 158
  22. def OAI.EisensteinCuspModThree.omegaPower line 164
  23. def OAI.EisensteinCuspModThree.unitPair line 165
  24. def OAI.EisensteinCuspModThree.cuspPair line 166
  25. def OAI.EisensteinCuspModThree.columnTop line 168
  26. def OAI.EisensteinCuspModThree.columnBottom line 170
  27. theorem OAI.EisensteinCuspModThree.primitive_column_three_cusps line 173
  28. def OAI.EisensteinCuspModThree.unitRepresentative line 186
  29. lemma OAI.EisensteinCuspModThree.unitRepresentative_value line 189
  30. lemma OAI.EisensteinCuspModThree.residue_omega line 193
  31. lemma OAI.EisensteinCuspModThree.residue_omega_sq line 200
  32. lemma OAI.EisensteinCuspModThree.unitRepresentative_residue line 204
  33. def OAI.EisensteinCuspModThree.cuspParameter line 211
  34. def OAI.EisensteinCuspModThree.cuspRepresentative line 212
  35. lemma OAI.EisensteinCuspModThree.cuspParameter_residue line 214
  36. def OAI.EisensteinCuspModThree.unitDiagonal line 217
  37. def OAI.EisensteinCuspModThree.columnRepresentative line 220
  38. lemma OAI.EisensteinCuspModThree.columnRepresentative_entry line 223
  39. lemma OAI.EisensteinCuspModThree.columnRepresentative_top_residue line 231
  40. lemma OAI.EisensteinCuspModThree.columnRepresentative_bottom_residue line 237
  41. lemma OAI.EisensteinCuspModThree.same_column_quotient_lower_zero line 243
  42. theorem OAI.EisensteinCuspModThree.three_cusp_decomposition line 251
  43. abbrev OAI.CubicEisenstein.PrimaryCoprimeDenominator line 299
  44. def OAI.CubicEisenstein.primaryDenominatorFromCoprime line 301
  45. lemma OAI.CubicEisenstein.primaryDenominatorFromCoprime_bijective line 308
  46. def OAI.CubicEisenstein.primaryDenominatorEquiv line 328
  47. def OAI.CubicEisenstein.unitLowerIntegral line 331
  48. lemma OAI.CubicEisenstein.hasSum_unitLowerIntegrals line 334
  49. lemma OAI.CubicEisenstein.unitLowerTerm_eq_shifted line 347
  50. lemma OAI.CubicEisenstein.unitLowerTerm_integrable line 357
  51. lemma OAI.CubicEisenstein.unitLowerTerm_fourier_integral line 363
  52. lemma OAI.CubicEisenstein.unitLowerGaussTerm_factor line 375
  53. lemma OAI.CubicEisenstein.unitLowerTwistedCoefficient_add line 407
  54. lemma OAI.CubicEisenstein.unitLowerTerm_weighted_translate line 419
  55. lemma OAI.CubicEisenstein.unitLowerIntegral_sum_translate line 470
  56. def OAI.CubicEisenstein.unitCuspIndexEquiv line 484
  57. lemma OAI.CubicEisenstein.unitDenominator_integral_formula line 498
  58. theorem OAI.CubicEisenstein.unitLowerEisenstein_fourier line 535
  59. lemma OAI.CubicKubota.levelTwo_entry_integer line 564
  60. def OAI.CubicKubota.integerUpper line 577
  61. def OAI.CubicKubota.integerLower line 578
  62. lemma OAI.CubicKubota.levelTwoComplexCharacter_primary line 580