OAI/Combinatorics/PolynomialVacuum/Algebra/RowCircuit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.homogeneousVector line 8
  2. def OAI.PolynomialVacuumAlgebra.frontCupData line 11
  3. def OAI.PolynomialVacuumAlgebra.finalCupData line 12
  4. def OAI.PolynomialVacuumAlgebra.reversedFinalData line 13
  5. def OAI.PolynomialVacuumAlgebra.frontFirstData line 14
  6. def OAI.PolynomialVacuumAlgebra.cupRowCircuit line 16
  7. def OAI.PolynomialVacuumAlgebra.homogeneousFusion line 19
  8. theorem OAI.PolynomialVacuumAlgebra.frontCupData_zero line 21
  9. theorem OAI.PolynomialVacuumAlgebra.frontCupData_one line 22
  10. theorem OAI.PolynomialVacuumAlgebra.finalCupData_left line 23
  11. theorem OAI.PolynomialVacuumAlgebra.finalCupData_right line 24
  12. theorem OAI.PolynomialVacuumAlgebra.front_skip line 26
  13. theorem OAI.PolynomialVacuumAlgebra.final_skip line 28
  14. theorem OAI.PolynomialVacuumAlgebra.front_fusion line 33
  15. theorem OAI.PolynomialVacuumAlgebra.final_fusion line 36
  16. theorem OAI.PolynomialVacuumAlgebra.front_insert line 39
  17. theorem OAI.PolynomialVacuumAlgebra.final_insert_rotation line 46
  18. theorem OAI.PolynomialVacuumAlgebra.rotateTensor_smul line 55
  19. theorem OAI.PolynomialVacuumAlgebra.polynomialVacuum_cupRow line 62