OAI/NumberTheory/PiExponent/Ampleness/AmpleProjectiveSections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.Geometry.isIso_restricted_section line 17
2. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.power_extension_ratio line 23
3. lemma OAI.PiExponentSeshadri.Geometry.coefficient_ratio line 37
4. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.power_section_embedding line 56
5. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.ample_projective_sections line 129