OAI/NumberTheory/OrdinaryCorrelations/HighTrace/OrderedSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.OrderedSelection line 25
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.orderedSelection_exists line 29
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.rootOffset line 60
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.firstExpression line 61
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.secondExpression line 62
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression line 63
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression_eval line 66
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression_nonzero line 73
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression_divides line 76
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.expression_earlier line 81
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.selected line 90
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarBlockPair.PathData.tests line 92