OAI/NumberTheory/DirichletL/Cusp/StaticReflectionPhases.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ShortDraftCusp.A4PhaseFromResidue_norm line 83
  2. lemma OAI.CubicEisenstein.sourceFrequencyAngle_norm_le_one line 96
  3. def OAI.CubicEisenstein.FixedCuspShape.reflectionStaticPhase line 105
  4. lemma OAI.CubicEisenstein.FixedCuspShape.reflectionStaticPhase_norm_le_one line 114
  5. lemma OAI.CubicEisenstein.FixedCuspShape.fixedCuspArrayWithPhase_reflectionStaticPhase line 121
  6. def OAI.CanonicalRowCompletion.reflectionConductor line 140
  7. def OAI.CanonicalRowCompletion.reflectionExcludedPrimes line 142
  8. lemma OAI.CanonicalRowCompletion.reflectionConductor_ne_zero line 145
  9. lemma OAI.CanonicalRowCompletion.reflectionConductor_ideal line 149
  10. lemma OAI.CanonicalRowCompletion.reflectionExcludedPrimes_bad line 159
  11. lemma OAI.CanonicalRowCompletion.reflectionExcludedPrimes_prime line 162
  12. lemma OAI.CanonicalRowCompletion.reflectionConductor_prime_mem line 167
  13. lemma OAI.CanonicalRowCompletion.reflectionExcludedGenerator_ne_zero line 176
  14. lemma OAI.CanonicalRowCompletion.reflectionExcludedGenerator_bad line 181
  15. lemma OAI.CanonicalRowCompletion.reflectionConductor_coprime_of_not_excluded line 190
  16. lemma OAI.CanonicalRowCompletion.reflectionConductor_coprime_primary line 201
  17. lemma OAI.CanonicalRowCompletion.reflectionLevelBound_ge_one line 208
  18. lemma OAI.CompletedGauss.prime_dvd_rowResidualPart_iff line 220
  19. lemma OAI.CompletedGauss.rowResidualPart_prime_fixed_mask line 229
  20. theorem OAI.CompletedGauss.completedReflectionPool_fixed_mask_filter line 237
  21. theorem OAI.CanonicalRowCompletion.goodMaskNonresidualPool_full_mask line 260
  22. theorem OAI.ShortDraftCusp.A3_ramified_character_of_relative_level line 284
  23. theorem OAI.ShortDraftCusp.A3_unramified_character_of_relative_level line 300
  24. theorem OAI.ShortDraftCusp.stratum_multiplier_of_cubic_factor line 324
  25. lemma OAI.ShortDraftCusp.A3_ramified_relative_primary line 392
  26. theorem OAI.ShortDraftCusp.A3_ramified_fixed_sector_character line 400
  27. theorem OAI.ShortDraftCusp.A3_unramified_fixed_sector_character line 415
  28. structure OAI.CubicEisenstein.ControlledStratumArithmetic line 433
  29. theorem OAI.CubicEisenstein.exists_controlledStratumArithmetic line 455
  30. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.frequency_congruence line 555
  31. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.numerator_congruence line 561
  32. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.numerator_mod_three line 568
  33. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.numerator_primary line 575
  34. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.denominator_primary line 580
  35. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.ramified_relative line 586
  36. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.unramified_relative line 600
  37. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.inverse_fixed line 612
  38. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.determinant line 621
  39. def OAI.CubicEisenstein.ControlledStratumArithmetic.ramifiedFixedFactor line 626
  40. def OAI.CubicEisenstein.ControlledStratumArithmetic.unramifiedFixedFactor line 630
  41. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.ramified_character line 633
  42. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.unramified_character line 651