OAI/AlgebraicGeometry/Seshadri/Jets/LocalQuotients.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_surjective_jetline 17 - lemma
OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_surjective_localJetline 38 - lemma
OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_localJet_kernelline 56 - lemma
OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_comap_maximalIdealline 73 - def
OAI.MaximalSeshadri.AlgebraicJets.finiteLocalTaylorQuotientline 83