OAI/AlgebraicGeometry/Seshadri/Projective/ProjectiveCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.ProjectiveBertini.affine_restriction_etale line 19
2. lemma OAI.MaximalSeshadri.ProjectiveBertini.awayToSection_awayι line 31
3. theorem OAI.MaximalSeshadri.ProjectiveBertini.closed_projective_affine_surjective line 42
4. lemma OAI.MaximalSeshadri.ProjectiveBertini.differentials_span_projective_chart line 66