OAI/NumberTheory/DirichletL/Eisenstein/RamifiedGaussSeries.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.ramifiedElement_ne_zero line 86
  2. lemma OAI.CubicEisenstein.ramifiedElement_level line 93
  3. lemma OAI.CubicEisenstein.ramified_denominator_condition line 97
  4. lemma OAI.CubicEisenstein.ramified_symbol_congr_mod_nine line 104
  5. lemma OAI.CubicEisenstein.primary_add_nine line 114
  6. def OAI.CubicEisenstein.ramifiedResidueAdd line 118
  7. lemma OAI.CubicEisenstein.ramifiedResidueAdd_injective line 126
  8. def OAI.CubicEisenstein.ramifiedResidueAddEquiv line 135
  9. lemma OAI.CubicEisenstein.residueAdditive_add line 143
  10. theorem OAI.CubicEisenstein.ramified_arithmetic_additive_eigen line 148
  11. theorem OAI.CubicEisenstein.ramified_arithmetic_support line 182
  12. lemma OAI.CubicEisenstein.ramified_primary_coprime line 215
  13. theorem OAI.CubicEisenstein.arithmeticResidueSum_ramified_split line 223
  14. lemma OAI.CubicEisenstein.ramifiedElement_absNorm line 232
  15. lemma OAI.CubicEisenstein.three_absNorm line 240
  16. theorem OAI.CubicEisenstein.ramified_arithmetic_norm_bound line 247
  17. def OAI.CubicEisenstein.ramifiedFrequencyBound line 263
  18. theorem OAI.CubicEisenstein.arithmeticResidueSum_ramified_index_bound line 265
  19. theorem OAI.CubicEisenstein.arithmeticDirichletTerm_ramified_vanish line 275
  20. abbrev OAI.CubicEisenstein.NonzeroLevelLower line 292
  21. def OAI.CubicEisenstein.ramifiedLower line 294
  22. lemma OAI.CubicEisenstein.ramifiedLower_ne_zero line 297
  23. lemma OAI.CubicEisenstein.ramifiedLower_level line 300
  24. lemma OAI.CubicEisenstein.ramifiedLower_span line 304
  25. def OAI.CubicEisenstein.ramifiedLowerMap line 309
  26. lemma OAI.CubicEisenstein.ramifiedLowerMap_injective line 312
  27. lemma OAI.CubicEisenstein.ramifiedLowerMap_surjective line 330
  28. def OAI.CubicEisenstein.ramifiedLowerEquiv line 359
  29. lemma OAI.CubicEisenstein.arithmeticDirichlet_support_nonzero line 362
  30. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_ramified_reindex line 369
  31. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_finite_ramified line 388
  32. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_gauss_expansion line 406
  33. theorem OAI.CubicEisenstein.cubicUnitGaussSum_phase_shift line 433
  34. def OAI.CubicEisenstein.unramifiedCubicGaussSeries line 462
  35. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_unramified_gauss line 465
  36. theorem OAI.CubicEisenstein.scatteringCoefficient_unramified_gauss line 486
  37. theorem OAI.CubicEisenstein.cubicUnitGaussSum_cube_shift line 502
  38. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_neg line 511
  39. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_lambda_pow line 520
  40. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_lambda_cube line 536
  41. theorem OAI.CubicEisenstein.unit_eq_sign_omega line 540
  42. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_nine_family line 556