OAI/NumberTheory/DirichletL/ChineseRemainder/FrequencyLifts.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftCRT.exists_strong_unit_frequency_lifts line 84
  2. theorem OAI.ShortDraftCRT.finiteCrossNumerator_fraction line 104
  3. theorem OAI.IdealGaussCRT.finite_fourier_sum_reindex line 134
  4. theorem OAI.FiniteGaussPhase.product_trace_fourier_sum_reindex line 160
  5. lemma OAI.FixedRayActiveSet.sum_nonzero_ite line 180
  6. def OAI.FixedRayActiveSet.activeStratum line 190
  7. theorem OAI.FixedRayActiveSet.sum_active_stratum line 194
  8. theorem OAI.FixedRayActiveSet.sum_by_active_strata line 221
  9. theorem OAI.LocalReflectionBrackets.canonical_active_stratum line 256
  10. lemma OAI.CubicEisenstein.ramifiedTraceLambda_dvd_of_lambda_dvd line 283
  11. def OAI.CubicEisenstein.paperLambdaQuotient line 296
  12. lemma OAI.CubicEisenstein.paperLambdaQuotient_mul line 299
  13. lemma OAI.CubicEisenstein.sourceCuspCoefficients_ramified_divisibility line 304
  14. def OAI.CubicEisenstein.sourceCuspPhaseNumerator line 312
  15. lemma OAI.CubicEisenstein.sourceCuspPhaseNumerator_embedding line 315
  16. lemma OAI.CubicEisenstein.sourceCuspPhaseNumerator_phase line 340
  17. def OAI.CanonicalRowCompletion.cubicTwoSupplement line 360
  18. def OAI.CanonicalRowCompletion.quadraticTwoSupplement line 365
  19. def OAI.CanonicalRowCompletion.twoSupplement line 368
  20. lemma OAI.CanonicalRowCompletion.cubicTwoSupplement_norm line 370
  21. lemma OAI.CanonicalRowCompletion.twoSupplement_norm line 375
  22. lemma OAI.CanonicalRowCompletion.cubicTwoSupplement_periodic line 382
  23. lemma OAI.CanonicalRowCompletion.twoSupplement_periodic line 395
  24. lemma OAI.CanonicalRowCompletion.idealRowHom_two_prime line 404
  25. theorem OAI.CanonicalRowCompletion.idealRowHom_two_formula line 449
  26. def OAI.CanonicalRowCompletion.supportedIdealRow line 473
  27. lemma OAI.CanonicalRowCompletion.supportedIdealRow_norm line 486
  28. lemma OAI.CanonicalRowCompletion.exists_supported_primary_unit line 492
  29. theorem OAI.CanonicalRowCompletion.supportedIdealRow_lambda_periodic line 504
  30. lemma OAI.CanonicalRowCompletion.supportedIdealRow_lambda_primary line 527
  31. lemma OAI.CanonicalRowCompletion.negative_two_prime line 538
  32. theorem OAI.CanonicalRowCompletion.exists_supported_numerator_factorization line 542
  33. lemma OAI.CanonicalRowCompletion.idealRowHom_argument_pow line 580
  34. def OAI.CanonicalRowCompletion.reciprocityPhaseMonoid line 586
  35. def OAI.CanonicalRowCompletion.numeratorBadTwist line 591
  36. lemma OAI.CanonicalRowCompletion.numeratorBadTwist_norm line 594
  37. lemma OAI.CanonicalRowCompletion.numeratorBadTwist_periodic line 609
  38. def OAI.CanonicalRowCompletion.movingNumeratorRow line 626
  39. lemma OAI.CanonicalRowCompletion.movingNumeratorRow_norm line 631
  40. lemma OAI.CanonicalRowCompletion.movingNumeratorRow_periodic line 634
  41. theorem OAI.CanonicalRowCompletion.idealRowHom_factor_numerator line 638