OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TestVacuous.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 21) line 21
2. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 27) line 27
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.test_vacuous line 29
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.test_unique line 43
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.origin line 55
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.origin_tests line 58
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.fullCylinder line 63
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.fullCylinder_holds line 67
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.mem_fullCylinder_support line 83
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.fullCylinder_width line 88
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.fullCylinder_integer line 97