OAI/Algebra/Determinantal/ProjectiveCounts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PermanentBorder.Multigraded.vandermondePairs line 9
2. theorem OAI.PermanentBorder.Multigraded.bilinear_simple_point_count_chart line 19
3. abbrev OAI.PermanentBorder.Multigraded.BlockAffineVariables line 62
4. def OAI.PermanentBorder.Multigraded.productAffineChart line 64
5. lemma OAI.PermanentBorder.Multigraded.productAffineChart_zero line 69
6. lemma OAI.PermanentBorder.Multigraded.productAffineChart_succ line 75
7. lemma OAI.PermanentBorder.Multigraded.productAffineChart_injective line 81
8. lemma OAI.PermanentBorder.Multigraded.productAffineChart_contDiff line 90
9. theorem OAI.PermanentBorder.Multigraded.bilinear_simple_point_count line 101
10. def OAI.PermanentBorder.Multigraded.BlockSeparated line 126
11. lemma OAI.PermanentBorder.Multigraded.projective_pair_separator line 130
12. theorem OAI.PermanentBorder.Multigraded.projective_interpolation line 152
13. theorem OAI.PermanentBorder.Multigraded.projective_points_le_pieceDim line 217
14. lemma OAI.PermanentBorder.Multigraded.eventually_blockSeparated line 265
15. theorem OAI.PermanentBorder.Multigraded.product_simple_point_bound_multichart line 285
16. theorem OAI.PermanentBorder.Multigraded.bilinear_simple_point_count_multichart line 374