OAI/NumberTheory/Jacobsthal/Renewal/OddPairCycleGrouping.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWindowContinue line 15
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWindowContinue_isFiniteKernel line 18
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWindowContinue_complete line 22
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveCapture line 28
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveContinue line 31
6. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveCapture_isFiniteKernel line 34
7. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveContinue_isFiniteKernel line 38
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveHit line 42
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveHit_eq_cycles line 45