OAI/NumberTheory/OrdinaryCorrelations/HighTrace/PrimeIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.primeIndex line 21
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.values_primeIndex line 23
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.used_mem_support line 26
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.PackedGaps line 31
5. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.GapCertificate line 34
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.selectedIndex line 46
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.modulusIndex line 48
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.template line 50
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.selected_relabel line 53
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.modulus_relabel line 55
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.expression_relabel line 57
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.formed line 63
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.template_admissible line 66
14. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.packed_gap_certificate line 76