OAI/Combinatorics/PolynomialVacuum/Algebra/InhomogeneousCircuit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.spectralVector line 9
  2. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.frontCupData line 12
  3. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.finalCupData line 13
  4. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.reversedFinalData line 14
  5. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.frontFirstData line 15
  6. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.cupRowCircuit line 17
  7. def OAI.PolynomialVacuumAlgebra.Inhomogeneous.spectralFusion line 20
  8. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.frontCupData_zero line 22
  9. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.frontCupData_one line 23
  10. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.finalCupData_left line 24
  11. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.finalCupData_right line 25
  12. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.front_skip line 27
  13. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.final_skip line 29
  14. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.front_fusion line 34
  15. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.final_fusion line 37
  16. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.front_insert line 40
  17. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.final_insert_rotation line 47
  18. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.rotateTensor_smul line 56
  19. theorem OAI.PolynomialVacuumAlgebra.Inhomogeneous.polynomialVacuum_cupRow line 63