OAI/NumberTheory/OrdinaryCorrelations/HighTrace/WitnessTestDescriptor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTestDescriptor line 18
2. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode line 19
3. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 23) line 23
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.rank line 35
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.selected line 36
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.modulus line 38
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.linear line 40
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.expression line 42
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.WellFormed line 45
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.embedding line 52
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.system line 54
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.wellFormed_of_relabel line 64
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.system_admissible_of_relabel line 86
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.descriptor_card line 106
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.WitnessTemplateCode.card_le line 113