OAI/NumberTheory/PiExponent/Ampleness/AmpleCurveDegreePositive.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveDegree.exists_ample_section_with_zero line 16
2. theorem OAI.PiExponent.CurveDegree.finite_nonempty_euler_pos line 39
3. theorem OAI.PiExponent.CurveDegree.section_euler_degree_pos line 51
4. theorem OAI.PiExponent.CurveDegree.ample_euler_degree_pos line 102
5. theorem OAI.PiExponent.CurveDegree.finite_line_cohomology_of_ample line 124
6. theorem OAI.PiExponent.CurveDegree.euler_degree_pos_of_ample line 131
7. theorem OAI.PiExponent.NumericalAmpleness.curveDegree_pos_of_ample line 144