OAI/NumberTheory/Jacobsthal/Sieve/ClosedEulerIndividualUpper.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseEuler.cutoffPrimes_eq_filtered_Ioc line 14
2. theorem OAI.Erdos970.ErdosInverseEuler.smallEuler_eq_primeProduct line 21
3. theorem OAI.Erdos970.ErdosInverseEuler.smallEuler_log_bounds line 30
4. theorem OAI.Erdos970.ErdosStoppedArithmetic.smallEuler_nat_primeProduct line 67
5. theorem OAI.Erdos970.ErdosStoppedArithmetic.smallEuler_prime_step line 71
6. theorem OAI.Erdos970.ErdosStoppedArithmetic.smallEuler_strict_le_two_closed line 91
7. theorem OAI.Erdos970.ErdosStoppedArithmetic.original_individual_upper_closed line 103