OAI/AlgebraicGeometry/Seshadri/Cohomology/ToricPresentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.PlaneCech.weight line 16
  2. def OAI.MaximalSeshadri.PlaneCech.vertexCone line 17
  3. lemma OAI.MaximalSeshadri.PlaneCech.direction_mem line 20
  4. lemma OAI.MaximalSeshadri.PlaneCech.vertexCone_add line 23
  5. lemma OAI.MaximalSeshadri.PlaneCech.clearing_monotone line 27
  6. theorem OAI.MaximalSeshadri.PlaneCech.exists_standard_generators line 37
  7. def OAI.MaximalSeshadri.PlaneCech.StandardGenerator line 57
  8. lemma OAI.MaximalSeshadri.PlaneCech.standard_at_zero line 60
  9. lemma OAI.MaximalSeshadri.PlaneCech.standard_at_one line 64
  10. lemma OAI.MaximalSeshadri.PlaneCech.standard_at_two line 68
  11. lemma OAI.MaximalSeshadri.PlaneCech.standard_vertex_zero line 72
  12. lemma OAI.MaximalSeshadri.PlaneCech.standard_vertex_one line 78
  13. lemma OAI.MaximalSeshadri.PlaneCech.standard_vertex_two line 90