OAI/NumberTheory/Jacobsthal/Primes/TagPrimePartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.ErdosStoppedTagSieve.mem_AP_canonical line 15
2. def OAI.Erdos970.ErdosStoppedTagSieve.intersectionPrimes line 23
3. theorem OAI.Erdos970.ErdosStoppedTagSieve.intersectionPrimes_eq_biUnion line 27
4. lemma OAI.Erdos970.ErdosStoppedTagSieve.intersection_AP_disjoint line 47
5. theorem OAI.Erdos970.ErdosStoppedTagSieve.intersectionPrimes_card line 61