OAI/NumberTheory/Jacobsthal/Conclusions/JacobsthalFinite.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.exists_offset_one line 19
2. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.prime_not_dvd_of_dvd_step line 33
3. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.progression_prime_hit_unique line 44
4. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.exists_coprime_progression line 63
5. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.factorial_isJacobsthalBound line 111
6. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.exists_isJacobsthalBound line 121
7. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.quadratic_of_eventually_quadratic line 125
8. theorem OAI.Erdos970.NumberTheoryLean.JacobsthalFinite.quadratic_iff_eventually_quadratic line 152