OAI/NumberTheory/DirichletL/Reciprocity/PrimaryCongruences.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicJacobiGlobal.integer_congruence_primary_cases line 83
  2. lemma OAI.CubicJacobiGlobal.symbol_three_shift_primary line 101
  3. lemma OAI.CubicJacobiGlobal.symbol_three_shift_integer line 109
  4. lemma OAI.CubicKubota.levelTwo_cube_phase_balance line 126
  5. lemma OAI.CubicKubota.levelTwo_comparison_character line 147
  6. lemma OAI.CubicKubota.levelTwo_cube_comparison_phase line 161
  7. lemma OAI.CubicEisenstein.ramified_cubicExp_nat_mul line 208
  8. lemma OAI.CubicEisenstein.ramified_trace_symbol line 215
  9. lemma OAI.CubicEisenstein.ramifiedSymbol_primaryCoord line 221
  10. def OAI.CubicEisenstein.ramifiedAffineParameter line 233
  11. lemma OAI.CubicEisenstein.ramifiedAffineParameter_coords line 235
  12. theorem OAI.CubicEisenstein.ramified_symbol_primary_shift line 246
  13. lemma OAI.CubicEisenstein.ramified_symbol_primary_shift_signed line 267
  14. lemma OAI.CubicEisenstein.ramifiedTraceLambda_square line 283
  15. lemma OAI.CubicEisenstein.ramified_character_coprime line 287
  16. lemma OAI.CubicEisenstein.affineCusp_phase_identity line 303
  17. def OAI.CubicEisenstein.ramifiedAffineGauss line 323
  18. lemma OAI.CubicEisenstein.ramifiedAffineGauss_factor line 330
  19. theorem OAI.CubicEisenstein.ramifiedAffineGauss_eq_unramified line 354
  20. def OAI.CubicEisenstein.eisensteinUnitRotation line 391
  21. def OAI.CubicEisenstein.eisensteinUnitEquiv line 410
  22. def OAI.CubicEisenstein.periodUnitEquiv line 416
  23. lemma OAI.CubicEisenstein.periodUnitEquiv_val line 419
  24. lemma OAI.CubicEisenstein.periodDomain_unit_rotation line 429
  25. theorem OAI.CubicEisenstein.period_integral_unit_rotation line 439
  26. theorem OAI.CubicEisenstein.period_integral_unit_affine line 451
  27. lemma OAI.CubicEisenstein.integral_upper_triangular_action line 470
  28. theorem OAI.CubicEisenstein.period_integral_upper_triangular line 498
  29. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_scaled_three_average_zero line 527
  30. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_scaled_three_average line 572
  31. theorem OAI.CubicEisenstein.cubicSource_scaled_three_average line 590
  32. lemma OAI.CubicEisenstein.lowerCuspMatrix_zero line 605
  33. lemma OAI.CubicEisenstein.cubicSource_scaled_periodic line 609
  34. lemma OAI.CubicEisenstein.sourceCuspRepresentative_periodic line 618
  35. def OAI.CubicEisenstein.sourcePrincipalCuspConstant line 628
  36. lemma OAI.CubicEisenstein.sourceCuspRepresentative_average line 631
  37. lemma OAI.CubicEisenstein.sourceCusp_average_of_decomposition line 641
  38. def OAI.CubicEisenstein.sourceCuspConstant line 658
  39. theorem OAI.CubicEisenstein.sourceCusp_average_all line 661
  40. theorem OAI.CubicEisenstein.sourceCuspConstant_decomposition line 671
  41. lemma OAI.CubicEisenstein.sourcePrincipalCuspConstant_ne_zero line 677
  42. lemma OAI.CubicEisenstein.sourceCuspConstant_zero_iff line 684
  43. lemma OAI.CubicEisenstein.sourceCuspConstant_left line 695
  44. lemma OAI.CubicEisenstein.sourceCuspConstant_upper_right line 701