OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FreeResidues.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeResidues line 19
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.binarySplit line 22
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.mergeResidues line 26
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.merge_fixed line 29
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.merge_free line 33
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.Compatible line 40
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.residualCylinder line 43
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.residualCylinder_holds line 47
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.fullCylinder_merge line 63
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.residual_support_iff line 77
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.residualCylinder_width line 82
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.residual_eq_bot_iff_support_fixed line 95
13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualEvents line 108
14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NoFixedForbidden line 112
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualEvents_proper line 117
16. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualEvents_width line 123
17. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residualEvents_avoidance line 129
18. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.VertexAllowed line 140
19. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.all_attachments_integer_iff line 143