OAI/NumberTheory/SiegelZeros/Intersection/RetainedIntersectionCycles.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent line 18
2. instance OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.(instance at line 27) line 27
3. theorem OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.homogeneous line 29
4. def OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.coordinate line 32
5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.coordinate_not_mem line 35
6. def OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.hilbertDegree line 40
7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.ProjectiveComponent.hilbertDegree_ge_one line 43
8. structure OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle line 51
9. instance OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.(instance at line 61) line 61
10. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.degree line 63
11. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.coefficientAt line 66
12. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.degree_nonneg line 70
13. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.coefficientAt_le_degree line 76
14. structure OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut line 91
15. instance OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.(instance at line 113) line 113
16. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.cutLength line 115
17. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.cutLength_spec line 118
18. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.next line 128
19. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.next_component line 134
20. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.next_coefficient line 137
21. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.CoversBelow line 140
22. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.parent_budget line 144
23. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCut.degree_next_le line 158
24. inductive OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCutHistory line 179
25. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCutHistory.degree_bound line 186
26. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.ProperCutHistory.coefficient_bound line 200