OAI/NumberTheory/DirichletL/GaussSum/ReflectionPool.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.reflectionSixInactiveWeight_support line 88
  2. lemma OAI.CompletedGauss.sixReflectionIndex_card line 109
  3. theorem OAI.CompletedGauss.completedReflectionPool_count_small_power line 113
  4. lemma OAI.CanonicalRowCompletion.actualSextic_sixth_one line 133
  5. lemma OAI.CanonicalRowCompletion.actualSextic_power_mod_six line 148
  6. lemma OAI.CanonicalRowCompletion.idealRowHom_eq_prime_count_product line 154
  7. lemma OAI.CanonicalRowCompletion.primeIndex_pairwise_coprime line 175
  8. theorem OAI.CanonicalRowCompletion.idealRowHom_eq_principalSexticRow line 180
  9. lemma OAI.CanonicalRowCompletion.coprimalityMask_good_part line 196
  10. lemma OAI.CanonicalRowCompletion.idealRowHom_sixth_denominator_mask line 212
  11. lemma OAI.CanonicalRowCompletion.mask_times_good_row line 218
  12. theorem OAI.CanonicalRowCompletion.rowTwist_eq_fixed_times_good_row_primary line 226
  13. lemma OAI.CanonicalRowCompletion.fixedNumeratorTwist_periodic line 247
  14. theorem OAI.CanonicalRowCompletion.exists_fixed_twist_principal_row line 256
  15. theorem OAI.CanonicalRowCompletion.rowTwist_completedT_eq_periodic line 288
  16. theorem OAI.ShortDraftCusp.exists_A4_local_units line 304
  17. theorem OAI.ShortDraftCusp.principal_stratum_multiplier line 368
  18. lemma OAI.CubicEisenstein.cuspRepresentative_zero_eq_one line 450
  19. def OAI.CubicEisenstein.principalCuspDatum line 456
  20. lemma OAI.CubicEisenstein.principalCuspDatum_matrix line 464
  21. lemma OAI.CubicEisenstein.principalCuspDatum_height line 469
  22. lemma OAI.CubicEisenstein.principalCuspDatum_dual line 473
  23. lemma OAI.CubicEisenstein.principalCuspDatum_multiplier line 479
  24. lemma OAI.CubicEisenstein.infinity_phaseNumerator_embedding line 486
  25. lemma OAI.CubicEisenstein.principalCuspDatum_phase line 492
  26. theorem OAI.CubicEisenstein.principal_stratum_smoothed line 514
  27. lemma OAI.ShortDraftCRT.exists_primary_unit_multiple line 602
  28. lemma OAI.ShortDraftCRT.normalize_coprime_pair line 613
  29. theorem OAI.ShortDraftCRT.exists_normalized_rational_cusp line 637