OAI/AlgebraicGeometry/Seshadri/Divisors/CartierSection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Geometry.LineBundle.restrict_sections_injective line 18
2. lemma OAI.MaximalSeshadri.Geometry.LineBundle.restricted_coefficient_injective line 32
3. lemma OAI.MaximalSeshadri.Geometry.LineBundle.section_coefficient_regular line 43
4. theorem OAI.MaximalSeshadri.Projective.sectionIdeal_effective_cartier line 66
5. lemma OAI.MaximalSeshadri.Projective.idealSheaf_mem_support_of_prime line 82