OAI/AlgebraicGeometry/Seshadri/Cohomology/PlaneFreeCech.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.PlaneCech.supported_distrib line 15
  2. lemma OAI.MaximalSeshadri.PlaneCech.pi_inf_sup_distrib line 24
  3. def OAI.MaximalSeshadri.PlaneCech.laurentSupported line 48
  4. lemma OAI.MaximalSeshadri.PlaneCech.laurentSupported_distrib line 51
  5. def OAI.MaximalSeshadri.PlaneCech.coneA line 66
  6. def OAI.MaximalSeshadri.PlaneCech.coneB line 67
  7. def OAI.MaximalSeshadri.PlaneCech.coneC line 68
  8. def OAI.MaximalSeshadri.PlaneCech.freeA line 70
  9. def OAI.MaximalSeshadri.PlaneCech.freeB line 72
  10. def OAI.MaximalSeshadri.PlaneCech.freeC line 74
  11. theorem OAI.MaximalSeshadri.PlaneCech.free_H1_zero line 77
  12. lemma OAI.MaximalSeshadri.PlaneCech.triangle_finite line 84
  13. theorem OAI.MaximalSeshadri.PlaneCech.free_H0_finite line 92