OAI/NumberTheory/Jacobsthal/Estimates/RealProgressionPoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosHyperbolaFourier.progressionPoint line 11
2. def OAI.Erdos970.ErdosHyperbolaFourier.lowerIndex line 13
3. def OAI.Erdos970.ErdosHyperbolaFourier.upperIndex line 16
4. def OAI.Erdos970.ErdosHyperbolaFourier.progressionPoints line 19
5. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoint_injective line 22
6. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoint_modEq line 28
7. theorem OAI.Erdos970.ErdosHyperbolaFourier.index_mem_iff line 33
8. theorem OAI.Erdos970.ErdosHyperbolaFourier.mem_progressionPoints_iff line 45
9. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoints_card line 63
10. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoints_count_error line 69