OAI/AlgebraicGeometry/Seshadri/Geometry/AffineBundleFinite.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MaximalSeshadri.Geometry.LineBundle.restrictline 17 - theorem
OAI.MaximalSeshadri.Geometry.LineBundle.affine_sections_finiteline 30 - theorem
OAI.MaximalSeshadri.Geometry.LineBundle.affine_open_sections_finiteline 53