OAI/NumberTheory/Jacobsthal/Paths/TagAffineConditions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.ErdosStoppedTagSieve.actual_bad_iff line 14
2. lemma OAI.Erdos970.ErdosStoppedTagSieve.mul_forbidden_iff line 35
3. lemma OAI.Erdos970.ErdosStoppedTagSieve.prime_cast_ne_zero_of_large line 42
4. theorem OAI.Erdos970.ErdosStoppedTagSieve.all_small_avoidance_iff line 52
5. theorem OAI.Erdos970.ErdosStoppedTagSieve.local_survivor_conditions line 98
6. def OAI.Erdos970.ErdosStoppedTagSieve.actualSurvivorPrimes line 114
7. theorem OAI.Erdos970.ErdosStoppedTagSieve.actualSurvivorPrimes_eq_sieve line 118