OAI/NumberTheory/Jacobsthal/Estimates/RationalCandidateSets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosAlignedProgression.parameterOf line 12
2. theorem OAI.Erdos970.ErdosAlignedProgression.parameterOf_spec line 14
3. theorem OAI.Erdos970.ErdosAlignedProgression.parameterValue_parameterOf line 24
4. theorem OAI.Erdos970.ErdosAlignedProgression.parameterOf_parameterValue line 32
5. def OAI.Erdos970.ErdosAlignedProgression.parameterCandidates line 50
6. theorem OAI.Erdos970.ErdosAlignedProgression.parameterOf_mem line 55
7. theorem OAI.Erdos970.ErdosAlignedProgression.parameterValue_mem line 73
8. theorem OAI.Erdos970.ErdosAlignedProgression.parameterCandidates_eq_image line 83
9. theorem OAI.Erdos970.ErdosAlignedProgression.parameterOf_injOn line 99
10. theorem OAI.Erdos970.ErdosAlignedProgression.modulusCount_eq_parameter_card line 111