OAI/AlgebraicGeometry/Seshadri/Divisors/SectionGermSystem.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Geometry.global_smul_eq_scalarEndline 23 - def
OAI.MaximalSeshadri.Geometry.affineCoefficientLinearline 31 - lemma
OAI.MaximalSeshadri.Geometry.affineCoefficientLinear_injectiveline 61 - lemma
OAI.MaximalSeshadri.Geometry.Surface.sections_finiteline 70 - lemma
OAI.MaximalSeshadri.Geometry.germCoefficients_eq_bivariateline 81 - lemma
OAI.MaximalSeshadri.Geometry.germCoefficients_injective_of_taylorline 88