OAI/NumberTheory/Jacobsthal/Sieve/TagCRTPeriodicity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.ErdosStoppedTagSieve.IntersectionIndex line 12
  2. def OAI.Erdos970.ErdosStoppedTagSieve.intersectionModuli line 13
  3. lemma OAI.Erdos970.ErdosStoppedTagSieve.intersection_moduli_product line 17
  4. lemma OAI.Erdos970.ErdosStoppedTagSieve.intersection_moduli_pairwise line 24
  5. def OAI.Erdos970.ErdosStoppedTagSieve.baseClasses line 43
  6. lemma OAI.Erdos970.ErdosStoppedTagSieve.baseClasses_card line 46
  7. lemma OAI.Erdos970.ErdosStoppedTagSieve.mem_baseClasses line 53
  8. def OAI.Erdos970.ErdosStoppedTagSieve.intersectionClasses line 67
  9. def OAI.Erdos970.ErdosStoppedTagSieve.intersectionResidues line 72
  10. lemma OAI.Erdos970.ErdosStoppedTagSieve.intersection_moduli_pos line 77
  11. theorem OAI.Erdos970.ErdosStoppedTagSieve.mem_intersectionResidues line 82
  12. theorem OAI.Erdos970.ErdosStoppedTagSieve.intersectionResidues_card line 101
  13. theorem OAI.Erdos970.ErdosStoppedTagSieve.intersectionResidues_reduced line 113
  14. theorem OAI.Erdos970.ErdosStoppedTagSieve.mod_mem_intersectionResidues line 139
  15. lemma OAI.Erdos970.ErdosStoppedTagSieve.totient_prime_product line 160
  16. theorem OAI.Erdos970.ErdosStoppedTagSieve.totient_intersection_modulus line 178