OAI/AlgebraicGeometry/Seshadri/Blowup/HartogsScheme.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Hartogs.spec_restriction_algebraMap line 15
2. theorem OAI.MaximalSeshadri.Hartogs.sections_injective_of_joint_localizations line 27
3. theorem OAI.MaximalSeshadri.Hartogs.nonempty_of_joint_localizations line 62
4. theorem OAI.MaximalSeshadri.Hartogs.domain_of_detecting_preintegral_open line 80
5. theorem OAI.MaximalSeshadri.Hartogs.principal_quotient_domain_of_preintegral_open line 96