OAI/NumberTheory/OrdinaryCorrelations/HighTrace/WitnessConfiguration.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration line 20
2. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessCodeSlot line 27
3. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessMetadata line 30
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.metadata line 36
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.primeCode line 40
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.rawCode line 46
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.rawCode_injective line 48
8. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.(instance at line 92) line 92
9. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.(instance at line 95) line 95
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.primeCode_support line 97
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.codeSlot_card line 131
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessConfiguration.metadata_card line 137