OAI/AlgebraicGeometry/Seshadri/Divisors/SectionComponent.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Geometry.pullback_zero_of_rangeline 23 - lemma
OAI.MaximalSeshadri.Geometry.affineCoefficient_basicOpenline 36 - lemma
OAI.MaximalSeshadri.Geometry.Surface.annihilated_subscheme_dimensionline 50 - lemma
OAI.MaximalSeshadri.Geometry.residue_image_one_leline 70 - theorem
OAI.MaximalSeshadri.Geometry.Surface.section_contains_curveline 89