OAI/NumberTheory/DirichletL/Hecke/PrimeExtraction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftHeckeBridge.dirichletTarget_of_normFiber_prefix_power line 38
  2. abbrev OAI.FiniteSFactor.O line 62
  3. theorem OAI.FiniteSFactor.extract_prime_of_squarefree line 64
  4. def OAI.FiniteSFactor.outsideWeight line 82
  5. theorem OAI.FiniteSFactor.outsideWeight_mul line 87
  6. def OAI.FiniteSFactor.fiber line 116
  7. theorem OAI.FiniteSFactor.mem_fiber line 119
  8. def OAI.FiniteSFactor.badFiber line 122
  9. def OAI.FiniteSFactor.goodFiber line 126
  10. theorem OAI.FiniteSFactor.mem_badFiber line 130
  11. theorem OAI.FiniteSFactor.mem_goodFiber line 135
  12. def OAI.FiniteSFactor.pick line 140
  13. theorem OAI.FiniteSFactor.pick_spec line 146
  14. theorem OAI.FiniteSFactor.squarefree_prime_fiber_sum line 154
  15. def OAI.FiniteSFactor.exceptPrimeCoeff line 200
  16. theorem OAI.FiniteSFactor.sum_filter_squarefree line 204
  17. theorem OAI.FiniteSFactor.restore_one_prime line 216
  18. theorem OAI.FiniteSFactor.restore_one_prime_all line 261
  19. def OAI.FiniteSFactor.outsideCoeff line 292
  20. theorem OAI.FiniteSFactor.outsideWeight_zero_of_not_squarefree line 296
  21. theorem OAI.FiniteSFactor.outsideWeight_prime_of_not_mem line 303
  22. theorem OAI.FiniteSFactor.exceptPrimeCoeff_outsideWeight line 315
  23. theorem OAI.FiniteSFactor.restore_insert_prime line 329
  24. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_zero_of_not_squarefree line 355
  25. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_mul_of_isRelPrime line 361
  26. theorem OAI.ShortDraftHeckeBridge.baseChange_restore_insert_prime line 368
  27. def OAI.DyadicTransfer.annularCutoff line 386
  28. theorem OAI.DyadicTransfer.annularCutoff_eq_zero_of_le_half line 389
  29. theorem OAI.DyadicTransfer.annularCutoff_eq_zero_of_two_le line 396
  30. theorem OAI.DyadicTransfer.partial_partition line 402
  31. theorem OAI.DyadicTransfer.partition_nat line 419
  32. def OAI.DyadicTransfer.expAnnularTest line 433
  33. theorem OAI.DyadicTransfer.expAnnularTest_eq_zero_of_le_half line 436
  34. theorem OAI.DyadicTransfer.expAnnularTest_eq_zero_of_two_le line 442
  35. theorem OAI.DyadicTransfer.expAnnularTest_norm_le line 448
  36. theorem OAI.DyadicTransfer.finite_exp_reassembly line 470
  37. theorem OAI.DyadicTransfer.finite_dyadic_piece_bound line 500
  38. theorem OAI.FiniteSFactor.restore_two_primes line 556