OAI/Combinatorics/Progressions/Lattices/BoundedPrimeDepthBudget.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.boundedPrimes line 14
  2. abbrev OAI.Erdos3.BoundedPrime line 16
  3. def OAI.Erdos3.boundedPrime line 18
  4. def OAI.Erdos3.boundedPrimeExponent line 20
  5. def OAI.Erdos3.boundedPrimePower line 22
  6. theorem OAI.Erdos3.mem_boundedPrimes line 24
  7. theorem OAI.Erdos3.boundedPrime_prime line 27
  8. theorem OAI.Erdos3.boundedPrime_le line 30
  9. theorem OAI.Erdos3.boundedPrime_injective line 33
  10. theorem OAI.Erdos3.boundedPrimeExponent_pos line 35
  11. theorem OAI.Erdos3.boundedPrimePower_pos line 38
  12. instance OAI.Erdos3.boundedPrimePower_neZero line 41
  13. theorem OAI.Erdos3.boundedPrimePower_le line 44
  14. theorem OAI.Erdos3.boundedPrimePower_maximal line 48
  15. theorem OAI.Erdos3.boundedPrime_card_le line 52
  16. theorem OAI.Erdos3.boundedPrimePower_pairwise line 62
  17. def OAI.Erdos3.boundedPrimeProduct line 79
  18. theorem OAI.Erdos3.boundedPrimeProduct_pos line 81
  19. theorem OAI.Erdos3.boundedPrimeProduct_captures line 84
  20. theorem OAI.Erdos3.natLog_ceil_exp_le_linear line 115
  21. theorem OAI.Erdos3.prime_natLog_tested_depth_le line 145
  22. theorem OAI.Erdos3.exists_testedPrimeDepth line 152