OAI/NumberTheory/PiExponent/Geometry/CurveCycleNumerical.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveCycle.componentEulerDegree_eq_curveDegree line 12
2. theorem OAI.PiExponent.CurveCycle.componentEulerDegree_nonneg_of_ample line 17
3. theorem OAI.PiExponent.CurveCycle.cycleEulerDegree_pos_of_ample line 26
4. theorem OAI.PiExponent.CurveCycle.cycleEulerDegree_margin line 43
5. theorem OAI.PiExponent.CurveCycle.tensor_euler_margin line 69
6. theorem OAI.PiExponent.CurveCycle.euler_degree_pos_of_ample_curve line 81