OAI/Algebra/Determinantal/AffineSelectors.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PermanentBorder.Selector.SelectorOuter line 8
  2. abbrev OAI.PermanentBorder.Selector.SelectorLabels line 9
  3. abbrev OAI.PermanentBorder.Selector.SelectorGateVars line 11
  4. def OAI.PermanentBorder.Selector.selectorSrc line 13
  5. def OAI.PermanentBorder.Selector.selectorDst line 17
  6. def OAI.PermanentBorder.Selector.selectorBaseWeight line 21
  7. def OAI.PermanentBorder.Selector.selectorWeight line 24
  8. def OAI.PermanentBorder.Selector.selectorMain line 26
  9. def OAI.PermanentBorder.Selector.selectorGate line 27
  10. def OAI.PermanentBorder.Selector.selectorMatrix line 29
  11. def OAI.PermanentBorder.Selector.selectorBoundary line 33
  12. def OAI.PermanentBorder.Selector.selectorSplitEquiv line 40
  13. def OAI.PermanentBorder.Selector.selectorSplit line 55
  14. theorem OAI.PermanentBorder.Selector.selectorSplit_C line 59
  15. theorem OAI.PermanentBorder.Selector.selectorSplit_main_left line 62
  16. theorem OAI.PermanentBorder.Selector.selectorSplit_main_right line 66
  17. theorem OAI.PermanentBorder.Selector.selectorSplit_gate_left line 70
  18. theorem OAI.PermanentBorder.Selector.selectorSplit_gate_right line 74
  19. theorem OAI.PermanentBorder.Selector.selectorSplit_coeff line 79
  20. def OAI.PermanentBorder.Selector.selectorBoundaryWeight line 89
  21. theorem OAI.PermanentBorder.Selector.selectorSplit_base line 93
  22. theorem OAI.PermanentBorder.Selector.selectorSplit_choices line 120
  23. theorem OAI.PermanentBorder.Selector.selectorSplit_boundary line 137
  24. theorem OAI.PermanentBorder.Selector.allOnes_block line 152
  25. theorem OAI.PermanentBorder.Selector.two_gates_count line 157
  26. theorem OAI.PermanentBorder.Selector.selector_boundary_coeff line 170
  27. theorem OAI.PermanentBorder.Selector.selector_matrix_permanent line 186
  28. theorem OAI.PermanentBorder.Selector.selector_matrix_card line 198
  29. theorem OAI.PermanentBorder.Selector.rename_inner line 209
  30. theorem OAI.PermanentBorder.Selector.rename_outer line 216
  31. theorem OAI.PermanentBorder.Selector.permanent_block_diagonal line 223
  32. theorem OAI.PermanentBorder.Selector.permanent_reindex_equiv line 236
  33. abbrev OAI.PermanentBorder.Selector.SelectorVertex line 250
  34. def OAI.PermanentBorder.Selector.selectorLinearEntries line 251
  35. theorem OAI.PermanentBorder.Selector.selectorMatrix_affine line 256
  36. theorem OAI.PermanentBorder.Selector.gadgetH_map line 270
  37. theorem OAI.PermanentBorder.Selector.selectorMatrix_map line 274
  38. def OAI.PermanentBorder.Selector.selectorCoefficientMatrix line 288
  39. theorem OAI.PermanentBorder.Selector.selectorLinearEntries_sum line 292
  40. theorem OAI.PermanentBorder.Selector.selector_polynomial_affine line 299
  41. theorem OAI.PermanentBorder.affineSubstitution_permanent line 318
  42. theorem OAI.PermanentBorder.polynomial_fromBlocks_affine line 329
  43. theorem OAI.PermanentBorder.exists_affine_permanent_padding line 343
  44. def OAI.PermanentBorder.coefficientPolynomial line 371
  45. def OAI.PermanentBorder.selectorScalar line 374
  46. theorem OAI.PermanentBorder.selectorScalar_ne_zero line 377
  47. theorem OAI.PermanentBorder.exists_selector_affine_projection line 382
  48. theorem OAI.PermanentBorder.HasBorderDeterminant.coefficientPolynomial line 407