OAI/Combinatorics/PolynomialVacuum/Algebra/ThreeSiteRestriction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.setFirstThree line 10
  2. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_0 line 12
  3. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_1 line 13
  4. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_2 line 14
  5. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_restore line 16
  6. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_update0 line 21
  7. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_update1 line 26
  8. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_update2 line 31
  9. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_pair01 line 35
  10. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_pair12 line 38
  11. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_swap01 line 42
  12. theorem OAI.PolynomialVacuumAlgebra.setFirstThree_swap12 line 47
  13. def OAI.PolynomialVacuumAlgebra.restrictThree line 53
  14. theorem OAI.PolynomialVacuumAlgebra.restrictThree_exchange1 line 56
  15. theorem OAI.PolynomialVacuumAlgebra.restrictThree_exchange2 line 67