OAI/Algebra/Determinantal/PlaneHilbert.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PermanentBorder.PlaneHilbert.Plane line 9
  2. abbrev OAI.PermanentBorder.PlaneHilbert.weight line 10
  3. abbrev OAI.PermanentBorder.PlaneHilbert.H line 11
  4. def OAI.PermanentBorder.PlaneHilbert.pieceCoordinates line 13
  5. instance OAI.PermanentBorder.PlaneHilbert.piece_finite line 21
  6. lemma OAI.PermanentBorder.PlaneHilbert.degree_fin_two line 24
  7. def OAI.PermanentBorder.PlaneHilbert.degreeIndexEquiv line 28
  8. lemma OAI.PermanentBorder.PlaneHilbert.finrank_piece line 52
  9. def OAI.PermanentBorder.PlaneHilbert.varMul line 71
  10. lemma OAI.PermanentBorder.PlaneHilbert.varMul_injective line 80
  11. lemma OAI.PermanentBorder.PlaneHilbert.piece_degreeOf_le line 86
  12. theorem OAI.PermanentBorder.PlaneHilbert.exists_varMul_outside line 90
  13. lemma OAI.PermanentBorder.PlaneHilbert.finrank_varMul_sup line 116
  14. abbrev OAI.PermanentBorder.PlaneHilbert.idealComponent line 132
  15. def OAI.PermanentBorder.PlaneHilbert.hVector line 136
  16. lemma OAI.PermanentBorder.PlaneHilbert.hVector_add_component line 139
  17. lemma OAI.PermanentBorder.PlaneHilbert.hVector_le line 144
  18. lemma OAI.PermanentBorder.PlaneHilbert.varMul_component_le line 148
  19. lemma OAI.PermanentBorder.PlaneHilbert.hVector_succ_le line 153
  20. lemma OAI.PermanentBorder.PlaneHilbert.hVector_succ_le_of_deficit line 162
  21. lemma OAI.PermanentBorder.PlaneHilbert.hVector_le_of_deficit line 176
  22. lemma OAI.PermanentBorder.PlaneHilbert.hVector_normalized_succ line 183
  23. lemma OAI.PermanentBorder.PlaneHilbert.homogeneous_factor_right line 198
  24. lemma OAI.PermanentBorder.PlaneHilbert.mulPiece_injective line 208
  25. abbrev OAI.PermanentBorder.PlaneHilbert.multiplicationRange line 215
  26. lemma OAI.PermanentBorder.PlaneHilbert.finrank_multiplicationRange line 219
  27. lemma OAI.PermanentBorder.PlaneHilbert.multiplicationRange_inf line 224
  28. lemma OAI.PermanentBorder.PlaneHilbert.multiplicationRange_le_component line 261
  29. theorem OAI.PermanentBorder.PlaneHilbert.hVector_coprime_bound line 267