OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ExceptionalCodeSlot.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ExceptionalCodeSlot line 21
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalPrimeCode line 23
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalShapeCode line 29
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalCodeSlot_card line 33
5. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalPrimeCode_support line 37
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.localTokenWeight_sameGeometry line 62
7. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalShapeCode_product line 66
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalTuple line 84
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalPick line 89
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalTuple_pick line 92
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalTuple_support line 98
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exceptionalCode_weight line 110