OAI/Algebra/Determinantal/FilteredPlane.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.PlaneHilbert.filtered line 9
  2. instance OAI.PermanentBorder.PlaneHilbert.filtered_finite line 13
  3. lemma OAI.PermanentBorder.PlaneHilbert.mem_filtered_succ line 19
  4. lemma OAI.PermanentBorder.PlaneHilbert.filtered_mono line 23
  5. lemma OAI.PermanentBorder.PlaneHilbert.homogeneous_mem_filtered line 33
  6. lemma OAI.PermanentBorder.PlaneHilbert.mul_X_filtered line 38
  7. def OAI.PermanentBorder.PlaneHilbert.topComponent line 51
  8. lemma OAI.PermanentBorder.PlaneHilbert.sub_topComponent_degree line 55
  9. lemma OAI.PermanentBorder.PlaneHilbert.sub_topComponent_mem_filtered line 71
  10. def OAI.PermanentBorder.PlaneHilbert.leadingMap line 86
  11. abbrev OAI.PermanentBorder.PlaneHilbert.leadingRelations line 90
  12. lemma OAI.PermanentBorder.PlaneHilbert.mem_leadingRelations line 93
  13. lemma OAI.PermanentBorder.PlaneHilbert.varMul_leadingRelations line 99
  14. lemma OAI.PermanentBorder.PlaneHilbert.leadingMap_range line 108
  15. def OAI.PermanentBorder.PlaneHilbert.filteredH line 121
  16. lemma OAI.PermanentBorder.PlaneHilbert.filteredH_add_rank line 124
  17. def OAI.PermanentBorder.PlaneHilbert.quotientH line 143
  18. lemma OAI.PermanentBorder.PlaneHilbert.quotientH_add_rank line 144
  19. lemma OAI.PermanentBorder.PlaneHilbert.quotientH_le line 147
  20. lemma OAI.PermanentBorder.PlaneHilbert.quotientH_succ_le_of_deficit line 152
  21. lemma OAI.PermanentBorder.PlaneHilbert.quotientH_le_of_deficit line 166
  22. lemma OAI.PermanentBorder.PlaneHilbert.quotientH_normalized line 174
  23. theorem OAI.PermanentBorder.PlaneHilbert.quotientH_coprime_bound line 183
  24. def OAI.PermanentBorder.PlaneHilbert.hSum line 206
  25. lemma OAI.PermanentBorder.PlaneHilbert.hSum_mono line 207
  26. lemma OAI.PermanentBorder.PlaneHilbert.hSum_succ line 210
  27. lemma OAI.PermanentBorder.PlaneHilbert.hSum_double_le line 212
  28. lemma OAI.PermanentBorder.PlaneHilbert.hSum_half_length line 224
  29. lemma OAI.PermanentBorder.PlaneHilbert.mul_filtered_by_homogeneous line 251
  30. lemma OAI.PermanentBorder.PlaneHilbert.multiplicationRange_le_leading line 266
  31. lemma OAI.PermanentBorder.PlaneHilbert.filtered_rank_eq_hSum line 287
  32. lemma OAI.PermanentBorder.PlaneHilbert.filtered_eq_top_of_tail line 298
  33. theorem OAI.PermanentBorder.PlaneHilbert.finite_interpolation_half line 317
  34. lemma OAI.PermanentBorder.PlaneHilbert.filtered_rank_double_le line 344
  35. abbrev OAI.PermanentBorder.LowPlane.Index line 357
  36. instance OAI.PermanentBorder.LowPlane.index_finite line 359
  37. instance OAI.PermanentBorder.LowPlane.index_fintype line 363
  38. lemma OAI.PermanentBorder.LowPlane.plane_degree line 365
  39. def OAI.PermanentBorder.LowPlane.indexEquiv line 370
  40. lemma OAI.PermanentBorder.LowPlane.card_index line 397
  41. lemma OAI.PermanentBorder.LowPlane.expansion line 401
  42. lemma OAI.PermanentBorder.LowPlane.remainder_expansion line 424
  43. lemma OAI.PermanentBorder.LinearParameters.independent_coefficients_mem line 442