OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SpecPrimeSlot.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecPrimeSlot line 17
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specSlotPrime line 20
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specSupport_iff_slot line 24
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specPrimeSlot_card line 40
5. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ListPrimeSlot line 55
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listSlotPrime line 58
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listSupport_iff_slot line 61
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listPrimeSlot_card line 73
9. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TaggedSlot line 81
10. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ExceptionalSlot line 85
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalPrime line 89
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalSupport line 94
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordTokens_nonempty line 98
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tagged_implies_used_none line 107
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.list_implies_untagged_none line 121
16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.mem_exceptionalSupport line 131
17. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.taggedGroupFactor_exact line 149
18. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tagged_product_slots line 160