OAI/NumberTheory/PiExponent/Ampleness/ExceptionalPowerSections.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Geometry.InvertibleLocal.pullback_frame_equation line 13
  2. theorem OAI.PiExponentSeshadri.Geometry.framed_section_range line 47
  3. theorem OAI.PiExponentSeshadri.Geometry.idealPower_restricted_range line 67
  4. def OAI.PiExponentSeshadri.Geometry.powerChartIdeal line 83
  5. abbrev OAI.PiExponentSeshadri.Geometry.powerSections line 88
  6. def OAI.PiExponentSeshadri.Geometry.idealPowerSectionsEquiv line 91
  7. theorem OAI.PiExponentSeshadri.Geometry.idealPowerSectionsEquiv_apply line 117