OAI/NumberTheory/Jacobsthal/Primes/PrimeProductOmissions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.reducedPrimes line 17
2. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.factor_bounds line 19
3. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.totient_euler line 24
4. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.euler_omissions_le line 30
5. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.cutoff_euler_eq line 55
6. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.prime_product_upper line 68
7. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeProductOmissions.reduced_product_upper line 84