OAI/Algebra/Determinantal/Multigraded.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PermanentBorder.Multigraded.Piece line 11
  2. abbrev OAI.PermanentBorder.Multigraded.componentQuotient line 13
  3. def OAI.PermanentBorder.Multigraded.ComponentClosed line 17
  4. lemma OAI.PermanentBorder.Multigraded.project_mul line 20
  5. lemma OAI.PermanentBorder.Multigraded.componentClosed_sup line 46
  6. lemma OAI.PermanentBorder.Multigraded.componentClosed_span_single line 55
  7. lemma OAI.PermanentBorder.Multigraded.componentClosed_bot line 63
  8. def OAI.PermanentBorder.Multigraded.componentMap line 68
  9. lemma OAI.PermanentBorder.Multigraded.componentMap_mk line 72
  10. def OAI.PermanentBorder.Multigraded.mulPiece line 76
  11. lemma OAI.PermanentBorder.Multigraded.mulPiece_val line 84
  12. def OAI.PermanentBorder.Multigraded.componentMul line 88
  13. lemma OAI.PermanentBorder.Multigraded.componentMul_mk line 94
  14. theorem OAI.PermanentBorder.Multigraded.finrank_product_split line 100
  15. structure OAI.PermanentBorder.Multigraded.FactorPair line 155
  16. def OAI.PermanentBorder.Multigraded.productIdeal line 163
  17. def OAI.PermanentBorder.Multigraded.splitBound line 167
  18. lemma OAI.PermanentBorder.Multigraded.productIdeal_closed line 173
  19. theorem OAI.PermanentBorder.Multigraded.finrank_le_splitBound line 181
  20. def OAI.PermanentBorder.Multigraded.blockWeight line 221
  21. lemma OAI.PermanentBorder.Multigraded.sum_blockWeight line 224
  22. lemma OAI.PermanentBorder.Multigraded.finite_block_degree line 234
  23. instance OAI.PermanentBorder.Multigraded.blockPiece_finite line 244
  24. def OAI.PermanentBorder.Multigraded.blockExponent line 258
  25. lemma OAI.PermanentBorder.Multigraded.weight_blockExponent line 262
  26. lemma OAI.PermanentBorder.Multigraded.prod_blockExponent line 269
  27. def OAI.PermanentBorder.Multigraded.componentEmbed line 281
  28. lemma OAI.PermanentBorder.Multigraded.componentEmbed_injective line 290
  29. theorem OAI.PermanentBorder.Multigraded.component_finrank_le_one_of_linear_relations line 301
  30. theorem OAI.PermanentBorder.Multigraded.component_finrank_zero_of_block_killed line 356