OAI/NumberTheory/Jacobsthal/Renewal/CompletedCycleFirstArrival.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_first_lintegralline 16 - lemma
OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_first_lintegralline 25 - theorem
OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_first_arrivalline 41 - theorem
OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturn_first_arrivalline 48