OAI/AlgebraicGeometry/Seshadri/Cohomology/TripleEvaluation.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MaximalSeshadri.Geometry.BaseSections.BaseHomline 18 - instance
OAI.MaximalSeshadri.Geometry.BaseSections.baseHomGroupline 19 - instance
OAI.MaximalSeshadri.Geometry.BaseSections.freeBaseHomGroupline 34 - instance
OAI.MaximalSeshadri.Geometry.BaseSections.freeBaseHomModuleline 38 - def
OAI.MaximalSeshadri.Geometry.BaseSections.freeBaseEquivline 42 - def
OAI.MaximalSeshadri.Geometry.BaseSections.homChartline 48 - lemma
OAI.MaximalSeshadri.Geometry.BaseSections.homChart_naturalline 53 - lemma
OAI.MaximalSeshadri.Geometry.BaseSections.homChart_rangeline 65 - lemma
OAI.MaximalSeshadri.Geometry.BaseSections.homChart_injectiveline 79