OAI/AlgebraicGeometry/Seshadri/Blowup/BlowupAffineSections.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Geometry.IsBlowup.preIsoline 17 - lemma
OAI.MaximalSeshadri.Geometry.IsBlowup.morphismRestrictline 27 - lemma
OAI.MaximalSeshadri.Geometry.presents_post_toSpecline 32 - theorem
OAI.MaximalSeshadri.Geometry.IsBlowup.affine_section_coverline 44 - lemma
OAI.MaximalSeshadri.Geometry.presents_morphismRestrictline 56