OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Cylinder.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.SourceCylinder.Cylinder line 17
2. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 20) line 20
3. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 24) line 24
4. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 38) line 38
5. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.support line 44
6. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.Holds line 48
7. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.Generates line 51
8. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.Private line 54
9. def OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.rank line 57
10. def OAI.OrdinaryCorrelations.SourceCylinder.Intersection line 63
11. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 66) line 66
12. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 71) line 71
13. instance OAI.OrdinaryCorrelations.SourceCylinder.(instance at line 74) line 74
14. def OAI.OrdinaryCorrelations.SourceCylinder.coefficient line 87
15. def OAI.OrdinaryCorrelations.SourceCylinder.retained line 90
16. def OAI.OrdinaryCorrelations.SourceCylinder.witnesses line 94
17. def OAI.OrdinaryCorrelations.SourceCylinder.avoidance line 99
18. def OAI.OrdinaryCorrelations.SourceCylinder.truncated line 103
19. def OAI.OrdinaryCorrelations.SourceCylinder.witnessCount line 107