OAI/Algebra/Determinantal/DegreeBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PermanentBorder.FrobeniusPlane.partial_degree line 10
2. lemma OAI.PermanentBorder.FrobeniusPlane.square_degree line 25
3. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_degree_bounds line 31
4. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_degree_le line 73
5. lemma OAI.PermanentBorder.FrobeniusPlane.subtract_top_degree line 90
6. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_top_even line 104
7. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_top_odd line 141
8. lemma OAI.PermanentBorder.FrobeniusPlane.homogeneous_not_unit line 185
9. lemma OAI.PermanentBorder.FrobeniusPlane.squarefree_even_pair line 193
10. lemma OAI.PermanentBorder.FrobeniusPlane.squarefree_odd_pair line 203
11. lemma OAI.PermanentBorder.FrobeniusPlane.squarefree_even_leading line 211
12. lemma OAI.PermanentBorder.FrobeniusPlane.squarefree_odd_leading line 228
13. def OAI.PermanentBorder.BinaryLeading.linear line 249
14. lemma OAI.PermanentBorder.BinaryLeading.linear_irreducible line 251
15. lemma OAI.PermanentBorder.BinaryLeading.linear_eval line 259
16. lemma OAI.PermanentBorder.BinaryLeading.linear_pair line 262
17. lemma OAI.PermanentBorder.BinaryLeading.squarefree_product line 271
18. lemma OAI.PermanentBorder.BinaryLeading.product_partial_coprime line 280
19. lemma OAI.PermanentBorder.BinaryLeading.product_nonzero line 301
20. lemma OAI.PermanentBorder.BinaryLeading.product_partial_nonzero line 307
21. lemma OAI.PermanentBorder.PlaneHilbert.leading_vanishing_mem line 320
22. theorem OAI.PermanentBorder.PlaneHilbert.finite_of_leading_pair line 327
23. def OAI.PermanentBorder.CurveFamily.halfIdeal line 350
24. lemma OAI.PermanentBorder.CurveFamily.halfIdeal_mem line 353
25. lemma OAI.PermanentBorder.CurveFamily.halfIdeal_even_finite line 358
26. lemma OAI.PermanentBorder.CurveFamily.halfIdeal_odd_finite line 373