OAI/Algebra/Determinantal/Gates.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.Selector.blockExponent line 9
  2. theorem OAI.PermanentBorder.Selector.mapDomain_block_apply line 13
  3. theorem OAI.PermanentBorder.Selector.blockExponent_apply line 24
  4. theorem OAI.PermanentBorder.Selector.blockExponent_injective line 30
  5. theorem OAI.PermanentBorder.Selector.coeff_independent_blocks line 36
  6. theorem OAI.PermanentBorder.Selector.eliminate_gadget_network line 66
  7. abbrev OAI.PermanentBorder.Selector.ExpandedVertex line 83
  8. abbrev OAI.PermanentBorder.Selector.InternalVertex line 84
  9. abbrev OAI.PermanentBorder.Selector.GadgetLabels line 85
  10. abbrev OAI.PermanentBorder.Selector.ExpandedLabels line 86
  11. def OAI.PermanentBorder.Selector.baseEdges line 88
  12. def OAI.PermanentBorder.Selector.vertexSplit line 91
  13. theorem OAI.PermanentBorder.Selector.allOnes_map_equiv line 106
  14. def OAI.PermanentBorder.Selector.expandedSrc line 114
  15. def OAI.PermanentBorder.Selector.expandedDst line 119
  16. def OAI.PermanentBorder.Selector.expandedWeight line 124
  17. def OAI.PermanentBorder.Selector.expandedMatrix line 130
  18. def OAI.PermanentBorder.Selector.splitPolynomial line 134
  19. theorem OAI.PermanentBorder.Selector.splitPolynomial_C line 139
  20. theorem OAI.PermanentBorder.Selector.splitPolynomial_outer_left line 143
  21. theorem OAI.PermanentBorder.Selector.splitPolynomial_outer_right line 147
  22. theorem OAI.PermanentBorder.Selector.splitPolynomial_inner_left line 151
  23. theorem OAI.PermanentBorder.Selector.splitPolynomial_inner_right line 155
  24. theorem OAI.PermanentBorder.Selector.split_edge line 160
  25. theorem OAI.PermanentBorder.Selector.gadget_factors line 169
  26. theorem OAI.PermanentBorder.Selector.split_expanded_edges line 198
  27. theorem OAI.PermanentBorder.Selector.block_three_ones line 222
  28. theorem OAI.PermanentBorder.Selector.splitPolynomial_top_coefficient line 236
  29. theorem OAI.PermanentBorder.Selector.expanded_permanent line 249
  30. theorem OAI.PermanentBorder.Selector.colored_diagonal_edges line 265
  31. theorem OAI.PermanentBorder.Selector.coeff_commAlgEquiv line 304
  32. theorem OAI.PermanentBorder.Selector.commAlgEquiv_map_C line 324
  33. theorem OAI.PermanentBorder.Selector.edgeProduct_map line 331
  34. def OAI.PermanentBorder.Selector.countIndex line 339
  35. def OAI.PermanentBorder.Selector.elementaryBoundary line 341
  36. def OAI.PermanentBorder.Selector.diagonalCoefficient line 343
  37. theorem OAI.PermanentBorder.Selector.swap_colored_edge_product line 349
  38. theorem OAI.PermanentBorder.Selector.two_color_coefficient line 371
  39. theorem OAI.PermanentBorder.Selector.diagonalCoefficient_boundary line 384
  40. def OAI.PermanentBorder.Selector.Gates.subsetExponent line 399
  41. theorem OAI.PermanentBorder.Selector.Gates.subsetExponent_apply line 403
  42. theorem OAI.PermanentBorder.Selector.Gates.subsetExponent_support line 409
  43. theorem OAI.PermanentBorder.Selector.Gates.subsetExponent_degree line 413
  44. theorem OAI.PermanentBorder.Selector.Gates.subsetExponent_multinomial line 418
  45. theorem OAI.PermanentBorder.Selector.Gates.coeff_gate_half line 429
  46. theorem OAI.PermanentBorder.Selector.Gates.sumRingEquiv_monomial line 440
  47. theorem OAI.PermanentBorder.Selector.Gates.coeff_nested line 443