OAI/Combinatorics/PolynomialVacuum/Algebra/NaturalRotation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.rotationIndex line 9
  2. def OAI.PolynomialVacuumAlgebra.natRotate line 11
  3. theorem OAI.PolynomialVacuumAlgebra.natRotate_zero line 13
  4. theorem OAI.PolynomialVacuumAlgebra.natRotate_succ line 14
  5. theorem OAI.PolynomialVacuumAlgebra.rotationIndex_injective line 16
  6. theorem OAI.PolynomialVacuumAlgebra.natRotate_update line 22
  7. theorem OAI.PolynomialVacuumAlgebra.natRotate_replacePair line 28
  8. theorem OAI.PolynomialVacuumAlgebra.natRotate_swapSite line 32
  9. theorem OAI.PolynomialVacuumAlgebra.natRotate_skipTwo line 49
  10. def OAI.PolynomialVacuumAlgebra.rotateTensor line 56
  11. def OAI.PolynomialVacuumAlgebra.cyclicTransform line 59
  12. def OAI.PolynomialVacuumAlgebra.NaturalCyclic line 62
  13. theorem OAI.PolynomialVacuumAlgebra.siteR_rotateTensor line 64
  14. theorem OAI.PolynomialVacuumAlgebra.cyclicTransform_exchange line 74
  15. def OAI.PolynomialVacuumAlgebra.rotatedPolynomial line 85
  16. def OAI.PolynomialVacuumAlgebra.cyclicDiscrepancy line 88
  17. theorem OAI.PolynomialVacuumAlgebra.eval_rotatedPolynomial line 91
  18. theorem OAI.PolynomialVacuumAlgebra.eval_cyclicDiscrepancy line 95
  19. theorem OAI.PolynomialVacuumAlgebra.cyclicDiscrepancy_exchange line 101