OAI/NumberTheory/Jacobsthal/Sieve/OddEulerCorrection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosOddEulerCorrection.correction line 10
2. theorem OAI.Erdos970.ErdosOddEulerCorrection.correction_nonneg line 12
3. theorem OAI.Erdos970.ErdosOddEulerCorrection.correction_le_one line 19
4. theorem OAI.Erdos970.ErdosOddEulerCorrection.correction_range line 24
5. theorem OAI.Erdos970.ErdosOddEulerCorrection.correction_finite_lower line 37
6. theorem OAI.Erdos970.ErdosOddEulerCorrection.odd_correction_product_lower line 52
7. theorem OAI.Erdos970.ErdosOddEulerCorrection.odd_two_class_factorization line 66
8. theorem OAI.Erdos970.ErdosOddEulerCorrection.odd_two_class_product_lower line 78