OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LabelPrimeSet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.labelPrimeSet line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.mem_labelPrimeSet line 21
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.labelPrimeSet_card line 30
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.labelPrimeSet_product line 37
5. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecMetadata line 46
6. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecCodeSlot line 47
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specMetadata line 49
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specPrimeCode line 54
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specPrimeCode_support line 61
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.data line 84
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.data_injective line 88
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.specification_code_injective line 111