OAI/AlgebraicGeometry/Seshadri/Divisors/AffineSectionQuotient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Geometry.global_sections_exact line 18
2. lemma OAI.MaximalSeshadri.Geometry.affine_global_sections_surjective line 38
3. def OAI.MaximalSeshadri.Geometry.frameCokernelMap line 55
4. lemma OAI.MaximalSeshadri.Geometry.frameCokernelMap_ker line 65
5. lemma OAI.MaximalSeshadri.Geometry.frameCokernelMap_surjective line 101
6. def OAI.MaximalSeshadri.Geometry.affine_section_quotient line 112