OAI/Algebra/Determinantal/LinearForms.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PermanentBorder.Multigraded.linearFormMap line 9
2. lemma OAI.PermanentBorder.Multigraded.linearFormMap_apply line 12
3. lemma OAI.PermanentBorder.Multigraded.linearFormMap_single line 16
4. def OAI.PermanentBorder.Multigraded.linearCoefficientSubspace line 21
5. theorem OAI.PermanentBorder.Multigraded.linear_relations_of_codimension_le_one line 24
6. theorem OAI.PermanentBorder.Multigraded.variables_mem_of_codimension_zero line 38
7. lemma OAI.PermanentBorder.Multigraded.linearIndependent_rect_vandermonde line 57
8. lemma OAI.PermanentBorder.Multigraded.linear_block_codimension_le line 66
9. abbrev OAI.PermanentBorder.Multigraded.BlockVariables line 90
10. def OAI.PermanentBorder.Multigraded.blockVar line 92
11. def OAI.PermanentBorder.Multigraded.blockLinearForm line 94
12. lemma OAI.PermanentBorder.Multigraded.blockLinearForm_homogeneous line 99
13. lemma OAI.PermanentBorder.Multigraded.labeled_codimension line 109
14. theorem OAI.PermanentBorder.Multigraded.labeled_leaf_bound line 125
15. def OAI.PermanentBorder.Multigraded.pieceDim line 165
16. def OAI.PermanentBorder.Multigraded.choiceIdeal line 168
17. def OAI.PermanentBorder.Multigraded.choiceShift line 174
18. lemma OAI.PermanentBorder.Multigraded.splitBound_eq_choiceSum line 179
19. lemma OAI.PermanentBorder.Multigraded.choice_mem_choiceIdeal line 202
20. def OAI.PermanentBorder.Multigraded.choiceCount line 219
21. lemma OAI.PermanentBorder.Multigraded.choiceCount_apply line 221
22. def OAI.PermanentBorder.Multigraded.mixedPolynomial line 227
23. lemma OAI.PermanentBorder.Multigraded.mixedPolynomial_eq_choices line 231
24. lemma OAI.PermanentBorder.Multigraded.mixed_coefficient_eq_count line 248
25. lemma OAI.PermanentBorder.Multigraded.choiceShift_le_length line 270
26. theorem OAI.PermanentBorder.Multigraded.comparison_piece_bound line 285
27. def OAI.PermanentBorder.Multigraded.homogeneousIdealMap line 336
28. lemma OAI.PermanentBorder.Multigraded.homogeneousIdealMap_val line 340
29. lemma OAI.PermanentBorder.Multigraded.homogeneousIdealMap_range line 344
30. lemma OAI.PermanentBorder.Multigraded.isWeightedHomogeneous_smul line 368
31. lemma OAI.PermanentBorder.Multigraded.homogeneousIdealMap_affine line 373
32. lemma OAI.PermanentBorder.Multigraded.pairProduct_mem_productIdeal line 390
33. lemma OAI.PermanentBorder.Multigraded.productIdeal_le line 400
34. lemma OAI.PermanentBorder.Multigraded.productIdeal_eq_span line 410
35. theorem OAI.PermanentBorder.Multigraded.affine_independent_polynomial line 427