OAI/Algebra/Determinantal/Selector.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.Selector.allOnes line 9
  2. theorem OAI.PermanentBorder.Selector.allOnes_apply line 12
  3. def OAI.PermanentBorder.Selector.edgeExponent line 14
  4. def OAI.PermanentBorder.Selector.occupancy line 17
  5. theorem OAI.PermanentBorder.Selector.occupancy_left line 21
  6. theorem OAI.PermanentBorder.Selector.occupancy_right line 30
  7. def OAI.PermanentBorder.Selector.permGraph line 38
  8. theorem OAI.PermanentBorder.Selector.mem_permGraph line 41
  9. theorem OAI.PermanentBorder.Selector.permGraph_injective line 45
  10. theorem OAI.PermanentBorder.Selector.occupancy_permGraph line 52
  11. theorem OAI.PermanentBorder.Selector.unique_column line 80
  12. theorem OAI.PermanentBorder.Selector.unique_row line 94
  13. theorem OAI.PermanentBorder.Selector.occupancy_eq_iff line 108
  14. def OAI.PermanentBorder.Selector.edgeProduct line 132
  15. theorem OAI.PermanentBorder.Selector.edgeProduct_expansion line 136
  16. theorem OAI.PermanentBorder.Selector.edgeProduct_permanent line 144
  17. theorem OAI.PermanentBorder.Selector.coeff_separate_univariate line 175
  18. theorem OAI.PermanentBorder.Selector.coeff_one_edge_factors line 203
  19. theorem OAI.PermanentBorder.Selector.coeff_row_edge_product line 218
  20. theorem OAI.PermanentBorder.Selector.sumRingEquiv_monomial line 238
  21. theorem OAI.PermanentBorder.Selector.coeff_nested line 241
  22. theorem OAI.PermanentBorder.Selector.edgeProduct_nested line 267
  23. theorem OAI.PermanentBorder.Selector.row_product_permanent line 284
  24. theorem OAI.PermanentBorder.Selector.row_product_diagonal line 293
  25. def OAI.PermanentBorder.Selector.graphMatrix line 310
  26. theorem OAI.PermanentBorder.Selector.graph_row_sum line 313
  27. theorem OAI.PermanentBorder.Selector.coeff_graph_edges line 326
  28. def OAI.PermanentBorder.Selector.threeOnes line 360
  29. def OAI.PermanentBorder.Selector.gadgetAfterRows line 362
  30. theorem OAI.PermanentBorder.Selector.coeff_gadgetAfterRows line 367
  31. def OAI.PermanentBorder.Selector.gadgetH line 392
  32. def OAI.PermanentBorder.Selector.gadgetRowEntries line 394
  33. def OAI.PermanentBorder.Selector.gadgetNested line 399
  34. theorem OAI.PermanentBorder.Selector.gadgetNested_rows line 403
  35. def OAI.PermanentBorder.Selector.gadgetEdges line 413
  36. theorem OAI.PermanentBorder.Selector.gadgetEdges_nested line 418
  37. theorem OAI.PermanentBorder.Selector.gadgetEdges_coefficient line 424