OAI/AlgebraicGeometry/Seshadri/Geometry/PencilCharts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Projective.affine_evaluation_finite line 19
2. lemma OAI.MaximalSeshadri.Projective.normalized_evalAway_polyToChart line 32
3. theorem OAI.MaximalSeshadri.Projective.finite_sectionsMorphism_chart line 52
4. instance OAI.MaximalSeshadri.Projective.boolChartUnique line 85
5. theorem OAI.MaximalSeshadri.Projective.finite_pencil_chart line 89