OAI/AlgebraicGeometry/Seshadri/Interpolation/RowCompression.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaximalSeshadri.Interpolation.RowIndex line 11
2. theorem OAI.MaximalSeshadri.Interpolation.compression_column_mem_span line 13
3. theorem OAI.MaximalSeshadri.Interpolation.compression_rank_to_powers line 42
4. theorem OAI.MaximalSeshadri.Interpolation.iteratedDeriv_affine_pow line 54
5. def OAI.MaximalSeshadri.Interpolation.verticalJetScale line 65
6. theorem OAI.MaximalSeshadri.Interpolation.verticalJetScale_column line 69
7. theorem OAI.MaximalSeshadri.Interpolation.compression_powers_to_original line 83
8. theorem OAI.MaximalSeshadri.Interpolation.affine_vertical_tuple_injective line 93
9. theorem OAI.MaximalSeshadri.Interpolation.compression_exists_tuple line 103