OAI/NumberTheory/OrdinaryCorrelations/HighTrace/AttachedMetadata.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedMetadata line 17
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.attachedMetadata line 19
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.attached_code_injective line 22
4. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ListMetadata line 34
5. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ListCodeSlot line 35
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listMetadata line 37
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listPrimeCode line 42
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.list_code_injective line 46
9. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listPrimeCode_support line 60
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specMetadata_card line 76
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listMetadata_card line 80
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listCodeSlot_card line 88