OAI/NumberTheory/PiExponent/Approximation/ClosedThickeningSections.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSeshadri.Geometry.globalSections_surjective_of_ext_one_zero line 16
2. theorem OAI.PiExponentSeshadri.Geometry.closed_appTop_surjective_of_ext_one_zero line 28
3. theorem OAI.PiExponentSeshadri.Geometry.subscheme_surjective_of_fullSupport line 43
4. theorem OAI.PiExponentSeshadri.Geometry.isAffine_of_fullSupport_of_ideal_ext_one_zero line 49