OAI/NumberTheory/Jacobsthal/Primes/PrimeProductLifting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.lineSub_eval line 11
2. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.eval_integer_cast line 23
3. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.divides_of_line_incidence line 33
4. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.zero_of_prime_product_large line 39
5. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.value_zero_of_incident_prime_product line 53