OAI/AlgebraicGeometry/Seshadri/Cohomology/LaurentSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.PlaneCech.laurentSupported_eq_span line 15
  2. lemma OAI.MaximalSeshadri.PlaneCech.supported_monomial_mul line 21
  3. lemma OAI.MaximalSeshadri.PlaneCech.supported_of_support line 34
  4. lemma OAI.MaximalSeshadri.PlaneCech.support_bound line 38
  5. lemma OAI.MaximalSeshadri.PlaneCech.freeA_stable line 57
  6. lemma OAI.MaximalSeshadri.PlaneCech.freeB_stable line 63
  7. lemma OAI.MaximalSeshadri.PlaneCech.freeC_stable line 69
  8. lemma OAI.MaximalSeshadri.PlaneCech.freeA_clearing line 78
  9. lemma OAI.MaximalSeshadri.PlaneCech.freeB_clearing line 89
  10. lemma OAI.MaximalSeshadri.PlaneCech.freeC_clearing line 100
  11. theorem OAI.MaximalSeshadri.PlaneCech.laurent_noetherian line 113
  12. theorem OAI.MaximalSeshadri.PlaneCech.submodule_top_finite line 117