OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LastEdge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.lastEdge line 19
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tailCandidates line 21
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tailCandidates_nonempty line 24
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tailStart line 34
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tail_labels line 37
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.before_tail_ne line 42
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tail_signs line 60
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tail_displacement line 80
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.not_dvd_signed_product line 95
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tailStart_pos line 112