OAI/AlgebraicGeometry/Seshadri/Analytic/PointCharts.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MaximalSeshadri.AlgebraicJets.presentationPointline 14 - lemma
OAI.MaximalSeshadri.AlgebraicJets.presentationPoint_applyline 24 - lemma
OAI.MaximalSeshadri.AlgebraicJets.presentationPoint_aevalline 29 - lemma
OAI.MaximalSeshadri.AlgebraicJets.presentationPoint_valline 40 - lemma
OAI.MaximalSeshadri.AlgebraicJets.evaluation_relationsline 45 - lemma
OAI.MaximalSeshadri.AlgebraicJets.presentationPoint_at_pointline 55 - theorem
OAI.MaximalSeshadri.AlgebraicJets.exists_analytic_zero_chartline 72 - theorem
OAI.MaximalSeshadri.AlgebraicJets.exists_analytic_point_chartline 98 - theorem
OAI.MaximalSeshadri.AlgebraicJets.exists_binary_point_chartline 143