OAI/NumberTheory/Jacobsthal/Primes/BadPrimeProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.prime_alignment line 12
2. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.nonaligned_prime_dvd_factor line 28
3. def OAI.Erdos970.ErdosPrimitiveIntercept.badPrimeFactors line 45
4. def OAI.Erdos970.ErdosPrimitiveIntercept.badPrimeProduct line 49
5. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.bad_product_dvd_factor line 52
6. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.structure_bound line 67