OAI/AlgebraicGeometry/Seshadri/Interpolation/LaurentJets.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.polynomials line 12
2. theorem OAI.MaximalSeshadri.Interpolation.momentJetZero_of_falling line 36
3. def OAI.MaximalSeshadri.Interpolation.indexedLaurent line 52
4. theorem OAI.MaximalSeshadri.Interpolation.indexedLaurent_mixed_deriv line 55
5. theorem OAI.MaximalSeshadri.Interpolation.indexedLaurent_deriv_scaled line 81
6. theorem OAI.MaximalSeshadri.Interpolation.indexedLaurent_jet_iff_moments line 94
7. theorem OAI.MaximalSeshadri.Interpolation.finiteJetColumn_indexedLaurent line 110
8. theorem OAI.MaximalSeshadri.Interpolation.finiteJetColumn_eq_zero_iff line 129
9. theorem OAI.MaximalSeshadri.Interpolation.shear_monomial line 145
10. theorem OAI.MaximalSeshadri.Interpolation.shearLaurent_jet line 150
11. theorem OAI.MaximalSeshadri.Interpolation.shear_tuple_injective line 164
12. theorem OAI.MaximalSeshadri.Interpolation.shear_jet_rank line 175
13. theorem OAI.MaximalSeshadri.Interpolation.diagonal_row_compression line 200
14. theorem OAI.MaximalSeshadri.Interpolation.indexedLaurent_nonzeroSupport line 221
15. theorem OAI.MaximalSeshadri.Interpolation.indexedLaurent_image line 231
16. theorem OAI.MaximalSeshadri.Interpolation.monomial_jet_rank_of_test line 241