OAI/AlgebraicGeometry/Seshadri/Interpolation/GermInterpolation.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MaximalSeshadri.Interpolation.initialExponentSetline 15 - theorem
OAI.MaximalSeshadri.Interpolation.exists_initial_basisline 18 - theorem
OAI.MaximalSeshadri.Interpolation.card_initialExponentSetline 56 - theorem
OAI.MaximalSeshadri.Interpolation.initial_monomial_jet_transferline 64 - theorem
OAI.MaximalSeshadri.Interpolation.rowTriangle_scaledline 97 - theorem
OAI.MaximalSeshadri.Interpolation.exists_node_weight_rangeline 102 - theorem
OAI.MaximalSeshadri.Interpolation.scaled_node_parametersline 112 - theorem
OAI.MaximalSeshadri.Interpolation.eventual_germ_jet_testline 130