OAI/AlgebraicGeometry/Seshadri/Geometry/PlaneChartAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.LaurentPlane.map_unit_zpow line 14
2. lemma OAI.MaximalSeshadri.LaurentPlane.lift_cone_left line 19
3. lemma OAI.MaximalSeshadri.LaurentPlane.lift_cone_right line 28
4. lemma OAI.MaximalSeshadri.LaurentPlane.lift_cone_top line 37
5. theorem OAI.MaximalSeshadri.LaurentPlane.finite_laurent_of_chart line 51