OAI/NumberTheory/PiExponent/Ampleness/AmpleGeneratedTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.IsAmple.tensor_of_section_cover line 17
  2. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.IsAmple.tensor_of_generatingSections line 40
  3. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.isAmple_of_generated_factor line 46
  4. def OAI.PiExponentSeshadri.Geometry.ampleInverseTwistCancel line 54
  5. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.isAmple_of_inverse_twist_section_cover line 60
  6. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.isAmple_of_inverse_twist_generatingSections line 69
  7. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.isAmple_of_inverse_moduleTwist_generatingSections line 76