OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ForwardSegment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.forwardSegment line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.forwardSegment_oriented line 45
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.forwardSegment_qualifies line 52
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.forwardSegment_support line 67
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.primitive_no_forwardSegment line 81
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.qualifies_prime_departure line 92
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.qualifies_prime_arrival line 97
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.primitive_no_prime_gap line 106