OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SpecificationTemplate.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationTemplate line 19
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationTemplate.expression line 24
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationTemplate.selected line 28
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationTemplate.WellFormed line 31
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.SpecificationTemplate.system line 34
6. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 47) line 47
7. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 51) line 51
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.extraName line 56
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.values_extraName line 60
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.codeTemplate line 65
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.codeTemplate_expression line 69
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.codeTemplate_formed line 77
13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.densitySize line 83
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.densitySize_nonneg line 86
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.suffix_log_size line 91
16. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.codeTemplate_admissible line 101