OAI/NumberTheory/OrdinaryCorrelations/HighTrace/UncutTreeEdges.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.uncutTreeEdges line 19
2. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath line 23
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.pathSign line 40
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.pathSign_mem line 43
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.path_step line 48
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.vertex_residue_eq line 59
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.departure_lit line 68
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.IsGap line 78
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.gap_prime_free line 84
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.gap_div_displacement line 96
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.specification line 103
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.gap_has_nonfixed line 126