OAI/NumberTheory/DirichletL/Eisenstein/FixedConductor.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.divisor_principal_norm_le line 84
  2. def OAI.CubicEisenstein.fixedCuspLevelBound line 95
  3. def OAI.CubicEisenstein.fixedCuspLevelScale line 98
  4. lemma OAI.CubicEisenstein.fixedCuspLevelBound_ge_one line 101
  5. lemma OAI.CubicEisenstein.fixedCuspLevelScale_pos line 109
  6. lemma OAI.CubicEisenstein.fixedCuspLevelScale_le line 118
  7. lemma OAI.CubicEisenstein.A4_traceLambda_pow_four line 137
  8. structure OAI.CubicEisenstein.PrincipalStratumArithmetic line 144
  9. theorem OAI.CubicEisenstein.exists_principalStratumArithmetic line 164
  10. lemma OAI.CubicEisenstein.PrincipalStratumArithmetic.frequency_congruence line 252
  11. def OAI.CubicEisenstein.PrincipalStratumArithmetic.datum line 269
  12. lemma OAI.CubicEisenstein.PrincipalStratumArithmetic.datum_point line 274
  13. def OAI.CubicEisenstein.PrincipalStratumArithmetic.smoothedValue line 283
  14. def OAI.CubicEisenstein.PrincipalStratumArithmetic.reflectedValue line 292
  15. theorem OAI.CubicEisenstein.PrincipalStratumArithmetic.smoothed_eq_reflected line 314
  16. theorem OAI.CubicEisenstein.exists_constructed_principal_reflection line 329
  17. abbrev OAI.CanonicalRowCompletion.BasePrimeIndex line 357
  18. abbrev OAI.CanonicalRowCompletion.FreePrimeIndex line 358
  19. def OAI.CanonicalRowCompletion.basePrimeRow line 360
  20. def OAI.CanonicalRowCompletion.freePrimeRow line 368
  21. lemma OAI.CanonicalRowCompletion.basePrimeRow_norm line 376
  22. lemma OAI.CanonicalRowCompletion.freePrimeRow_norm line 384
  23. lemma OAI.CanonicalRowCompletion.basePrimeRow_periodic line 392
  24. lemma OAI.CanonicalRowCompletion.idealRowHom_fixed_conductor_split line 402
  25. lemma OAI.CanonicalRowCompletion.freePrimeIndex_pairwise_coprime line 410
  26. lemma OAI.CanonicalRowCompletion.freePrimeIndex_coprime line 415
  27. lemma OAI.CanonicalRowCompletion.freePrimeProduct_coprime line 423
  28. lemma OAI.CanonicalRowCompletion.freePrimeRow_eq_principalSexticRow line 427
  29. theorem OAI.CanonicalRowCompletion.fixed_conductor_absorb_shared_primes line 437
  30. lemma OAI.CanonicalRowCompletion.freePrimeRow_periodic line 461
  31. lemma OAI.CanonicalRowCompletion.fixedFreeRow_periodic line 471
  32. lemma OAI.CanonicalRowCompletion.fixedFreeRow_norm line 479
  33. theorem OAI.CanonicalRowCompletion.exists_actual_coprime_row line 485
  34. theorem OAI.CanonicalRowCompletion.exists_actual_coprime_completed_row line 500
  35. def OAI.CanonicalRowCompletion.fixedQuotientValue line 526
  36. lemma OAI.CanonicalRowCompletion.fixedQuotientValue_mk line 528
  37. lemma OAI.CanonicalRowCompletion.fixedQuotientValue_norm line 533
  38. def OAI.CanonicalRowCompletion.goodMaskMovingIdeal line 542
  39. lemma OAI.CanonicalRowCompletion.goodMaskMovingIdeal_supported line 544
  40. lemma OAI.CanonicalRowCompletion.good_odd_prime_two_not_mem line 549
  41. lemma OAI.CanonicalRowCompletion.count_span_eq_zero_of_not_mem line 555
  42. lemma OAI.CanonicalRowCompletion.good_factor_count line 566
  43. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_count line 584
  44. lemma OAI.CanonicalRowCompletion.squarefree_prime_count_indicator line 607
  45. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_exponent line 620
  46. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_generator_exponent line 633