OAI/NumberTheory/DirichletL/GaussSum/ActiveReindexing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.active_product_admissible_equiv line 82
  2. theorem OAI.CompletedGauss.residual_bracket_extracted_admissible line 94
  3. theorem OAI.CompletedGauss.residual_coefficient_eq_canonical_admissible line 105
  4. theorem OAI.CompletedGauss.residual_equiv_coefficient_admissible line 128
  5. theorem OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_tsum_eq_rawValue_at_row line 173
  6. theorem OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspBranch_value_eq_rawValue line 248
  7. theorem OAI.CubicEisenstein.FixedFourierGeometry.sixPhaseFixedCuspBranch_value_eq_geometric_rawValue line 273
  8. def OAI.CompletedGauss.FreeReflection.supportActivePoolEquiv line 304
  9. lemma OAI.CompletedGauss.FreeReflection.supportActivePoolEquiv_val line 313
  10. lemma OAI.CompletedGauss.FreeReflection.supportActivePoolEquiv_symm_val line 317
  11. lemma OAI.CompletedGauss.FreeReflection.supportActivePoolEquiv_label line 321
  12. def OAI.CompletedGauss.FreeReflection.encodedActivePoolEquiv line 326
  13. lemma OAI.CompletedGauss.FreeReflection.encodedActivePoolEquiv_val line 340
  14. lemma OAI.CompletedGauss.FreeReflection.encodedActivePoolEquiv_label line 343
  15. lemma OAI.CompletedGauss.FreeReflection.encodedActivePoolEquiv_divisor line 353
  16. def OAI.CanonicalRowCompletion.ActualFiber.activeModelPrimeEquiv line 379
  17. lemma OAI.CanonicalRowCompletion.ActualFiber.splitIndex_prime_val line 387
  18. lemma OAI.CanonicalRowCompletion.ActualFiber.splitIndex_local_exponent line 393
  19. lemma OAI.CanonicalRowCompletion.ActualFiber.activeModelPrimeEquiv_prime_val line 401
  20. lemma OAI.CanonicalRowCompletion.ActualFiber.activeModelPrimeEquiv_span line 408
  21. lemma OAI.CanonicalRowCompletion.ActualFiber.activeModelPrimeEquiv_exponent line 417
  22. lemma OAI.CubicEisenstein.finiteAdditiveFourierCoeff_zero line 440
  23. lemma OAI.CubicEisenstein.prime_zeroFourier_norm_formula line 447
  24. lemma OAI.CompletedGauss.FreeReflection.reflectionInactiveStratumWeight_formula line 470
  25. theorem OAI.CanonicalRowCompletion.GoodMaskRowData.inactive_source_reindex line 498
  26. theorem OAI.CubicEisenstein.sum_fixedReflectionRay line 573
  27. theorem OAI.CubicEisenstein.sum_fixedReflectionRayFin line 593