OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DivisorPathTemplate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate line 19
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.selected line 24
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.expression line 25
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.WellFormed line 27
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.embedding line 30
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.system line 32
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathTemplate.card_le line 46
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.tests line 61
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.admissible line 73
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.selectedIndex line 77
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.template line 79
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.selected_relabel line 81
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.expression_relabel line 83
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.formed line 89
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.template_admissible line 98
16. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GoodDivisorPathTemplate line 108
17. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.divisorPathTemplateMass line 109
18. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.divisorPathTemplateMass_le line 113