OAI/AlgebraicGeometry/Seshadri/Divisors/LinearSections.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Frames.coefficient_addline 17 - lemma
OAI.MaximalSeshadri.Frames.coefficient_zeroline 22 - lemma
OAI.MaximalSeshadri.Frames.coefficient_sumline 27 - lemma
OAI.MaximalSeshadri.Frames.restrictSection_addline 35 - lemma
OAI.MaximalSeshadri.Frames.restrictSection_zeroline 40 - lemma
OAI.MaximalSeshadri.Frames.restrictSection_sumline 45 - lemma
OAI.MaximalSeshadri.Frames.coefficient_scalar_compline 53 - lemma
OAI.MaximalSeshadri.Frames.coefficient_restrict_scalar_compline 59