OAI/NumberTheory/PiExponent/Ampleness/ReesExceptional.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.ReesGrading.generators_adjoin line 13
  2. lemma OAI.PiExponentSeshadri.ReesGrading.generators_adjoin_zero line 27
  3. lemma OAI.PiExponentSeshadri.ReesGrading.iSup_generator_basicOpen line 42
  4. def OAI.PiExponentSeshadri.ReesGrading.chartCover line 47
  5. lemma OAI.PiExponentSeshadri.ReesGrading.chartCover_projection line 59
  6. def OAI.PiExponentSeshadri.Geometry.lineBundleOfCover line 70
  7. def OAI.PiExponentSeshadri.Geometry.idealLineBundle line 77
  8. def OAI.PiExponentSeshadri.ReesGrading.exceptionalIdeal line 94
  9. def OAI.PiExponentSeshadri.ReesGrading.chartEquation line 97
  10. lemma OAI.PiExponentSeshadri.ReesGrading.exceptional_chart line 100
  11. lemma OAI.PiExponentSeshadri.ReesGrading.chartEquation_regular line 108
  12. def OAI.PiExponentSeshadri.ReesGrading.exceptionalLineBundle line 118
  13. def OAI.PiExponentSeshadri.ReesGrading.exceptionalInclusion line 122
  14. instance OAI.PiExponentSeshadri.ReesGrading.exceptionalInclusion_mono line 125
  15. lemma OAI.PiExponentSeshadri.ReesGrading.exceptional_presents line 130
  16. theorem OAI.PiExponentSeshadri.ReesGrading.exceptional_invertible line 137