OAI/AlgebraicGeometry/Seshadri/Divisors/SectionIdeal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Projective.sectionIdeal line 19
2. lemma OAI.MaximalSeshadri.Projective.sectionIdeal_restrict line 24
3. lemma OAI.MaximalSeshadri.Projective.sectionIdeal_on line 32
4. lemma OAI.MaximalSeshadri.Projective.coefficient_span_frame line 64
5. lemma OAI.MaximalSeshadri.Projective.sectionIdeal_on_frame line 71