OAI/Algebra/Determinantal/GateCoefficients.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.Selector.Gates.sumRingEquiv_rename_inl line 7
  2. theorem OAI.PermanentBorder.Selector.Gates.sumRingEquiv_rename_inr line 13
  3. theorem OAI.PermanentBorder.Selector.Gates.coeff_sum_product line 19
  4. theorem OAI.PermanentBorder.Selector.Gates.coeff_separate_univariate line 29
  5. theorem OAI.PermanentBorder.Selector.Gates.coeff_one_edge_factors line 57
  6. theorem OAI.PermanentBorder.Selector.Gates.coeff_row_edge_product line 72
  7. def OAI.PermanentBorder.Selector.Gates.gateOuter line 92
  8. theorem OAI.PermanentBorder.Selector.Gates.coeff_gateOuter line 95
  9. def OAI.PermanentBorder.Selector.Gates.gateCrossEntries line 101
  10. def OAI.PermanentBorder.Selector.Gates.gateCrossEdges line 107
  11. theorem OAI.PermanentBorder.Selector.Gates.gateCrossEdges_coefficient line 112
  12. theorem OAI.PermanentBorder.Selector.Gates.subsetExponent_add_compl line 118
  13. theorem OAI.PermanentBorder.Selector.Gates.coeff_gate_prescribed_distinguished line 123
  14. def OAI.PermanentBorder.Selector.Gates.pairedExponent line 138
  15. theorem OAI.PermanentBorder.Selector.Gates.sum_pairedExponent line 141
  16. theorem OAI.PermanentBorder.Selector.Gates.independent_boundary_expansion line 151
  17. theorem OAI.PermanentBorder.Selector.Gates.univariate_boundary_coefficient line 160
  18. theorem OAI.PermanentBorder.Selector.Gates.gate_filters_prescribed_count line 170
  19. def OAI.PermanentBorder.Selector.Gates.blockExponent line 193
  20. theorem OAI.PermanentBorder.Selector.Gates.mapDomain_block_apply line 197
  21. theorem OAI.PermanentBorder.Selector.Gates.blockExponent_apply line 208
  22. theorem OAI.PermanentBorder.Selector.Gates.blockExponent_injective line 214
  23. theorem OAI.PermanentBorder.Selector.Gates.coeff_independent_blocks line 220
  24. theorem OAI.PermanentBorder.Selector.Gates.gate_network_filters line 249
  25. def OAI.PermanentBorder.Selector.Gates.allOnes line 264
  26. theorem OAI.PermanentBorder.Selector.Gates.allOnes_map_equiv line 266
  27. theorem OAI.PermanentBorder.Selector.Gates.allOnes_sum line 273
  28. theorem OAI.PermanentBorder.Selector.Gates.subset_univ_ones line 276
  29. def OAI.PermanentBorder.Selector.Gates.sumSquareSplit line 280
  30. def OAI.PermanentBorder.Selector.Gates.fullGateEdges line 294
  31. theorem OAI.PermanentBorder.Selector.Gates.full_gate_split line 300
  32. theorem OAI.PermanentBorder.Selector.Gates.full_gate_count line 326