OAI/NumberTheory/Jacobsthal/Estimates/ReturnCompletionAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturn_succ_comp line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnLaw_first_step line 20
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitOrReturn_comp_captured line 37
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitOrReturn_comp_killed line 50
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.complete_first_pair line 61
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitOrReturn_translation line 65