OAI/NumberTheory/DirichletL/Eisenstein/ConjugateLevelAction.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.globalKubotaKernel_conjugate_mem line 86
  2. def OAI.CubicEisenstein.kernelConjugate line 97
  3. lemma OAI.CubicEisenstein.kernelConjugate_coe line 104
  4. lemma OAI.CubicEisenstein.level_action_respects_kernel line 107
  5. def OAI.CubicEisenstein.kernelLevelAction line 119
  6. lemma OAI.CubicEisenstein.kernelLevelAction_mk line 122
  7. lemma OAI.CubicEisenstein.kernelLevelAction_one line 126
  8. lemma OAI.CubicEisenstein.kernelLevelAction_mul line 132
  9. lemma OAI.CubicEisenstein.kernelLevelAction_continuous line 140
  10. def OAI.CubicEisenstein.kernelLevelHomeomorph line 143
  11. lemma OAI.CubicEisenstein.kernelLevelAction_eisenstein line 151
  12. lemma OAI.CubicEisenstein.kernelLevelAction_seed line 159
  13. lemma OAI.CubicEisenstein.kernelLevelAction_defect line 164
  14. lemma OAI.CubicEisenstein.kernelLevelAction_fundamentalDomain line 169
  15. lemma OAI.CubicEisenstein.kernelLevelAction_measurePreserving line 187
  16. def OAI.CubicEisenstein.kernelLevelPullback line 215
  17. lemma OAI.CubicEisenstein.kernelLevelPullback_ae_eq line 218
  18. lemma OAI.CubicEisenstein.kernelLevelPullback_one line 223
  19. lemma OAI.CubicEisenstein.kernelLevelPullback_comp line 228
  20. lemma OAI.CubicEisenstein.kernelLevelPullback_surjective line 238
  21. def OAI.CubicEisenstein.kernelLevelUnitary line 243
  22. lemma OAI.CubicEisenstein.kernelLevelUnitary_apply line 246
  23. lemma OAI.CubicEisenstein.kernelLevelPullback_defect line 249
  24. lemma OAI.CubicEisenstein.kernelLevelPullback_of_remainder_ae line 261
  25. lemma OAI.CubicEisenstein.kernelCorrection_character_of_initial_overlap line 275
  26. lemma OAI.CubicEisenstein.thetaApproach_tendsto_complex_punctured line 305
  27. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_character_of_initial_overlap line 321
  28. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_eq_of_initial_overlap line 351
  29. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_nonzero_character_of_initial_overlap line 371
  30. def OAI.QuadraticAllOddCRT.quadraticRayExponent line 395
  31. def OAI.QuadraticAllOddCRT.fourthRoot line 399
  32. lemma OAI.QuadraticAllOddCRT.fourthRoot_add line 401
  33. lemma OAI.QuadraticAllOddCRT.quadraticRayValue_eq_fourthRoot line 408
  34. def OAI.QuadraticAllOddCRT.quadraticRaySign line 423
  35. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_mul_left line 429
  36. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_mul_right line 437
  37. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_symm line 445
  38. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_sq line 449
  39. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_exponent line 455
  40. lemma OAI.QuadraticAllOddCRT.quadraticRaySign_root line 463
  41. lemma OAI.QuadraticAllOddCRT.odd_mul line 470
  42. theorem OAI.QuadraticAllOddCRT.quadraticRayValue_mul line 474
  43. lemma OAI.QuadraticAllOddCRT.quadraticRayPair_eq_sign line 481
  44. lemma OAI.CanonicalRowCompletion.supported_factors_good line 504
  45. lemma OAI.CanonicalRowCompletion.idealRowHom_one_supported line 510
  46. lemma OAI.CanonicalRowCompletion.supported_prime_data line 514
  47. lemma OAI.CanonicalRowCompletion.supported_residue_odd line 519
  48. theorem OAI.CanonicalRowCompletion.idealRowHom_prime_reciprocity line 522
  49. def OAI.CanonicalRowCompletion.sexticReciprocityPhase line 580
  50. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_mul_left line 583
  51. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_mul_right line 587
  52. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_one_right line 591
  53. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_one_left line 601
  54. lemma OAI.CanonicalRowCompletion.idealRowHom_prime_primary_reciprocity line 607
  55. theorem OAI.CanonicalRowCompletion.idealRowHom_primary_reciprocity line 634
  56. theorem OAI.CanonicalRowCompletion.idealRowHom_primary_reciprocity_ray line 660
  57. theorem OAI.CanonicalRowCompletion.idealRowHom_ideal_reciprocity line 668