OAI/MathematicalPhysics/PEPSMove/PhysicalCoordinates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.unionJoin line 16
  2. def OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.unionEquiv line 20
  3. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.unionJoin_left line 36
  4. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.unionJoin_right line 41
  5. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.liftBetween_union_right line 47
  6. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.density_union_ptrL line 85
  7. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.coefficient_gram line 95
  8. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.coefficient_action line 104
  9. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.coefficient_action_reindex line 110
  10. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.coefficient_hsEnergy line 119
  11. def OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.complementJoin line 137
  12. def OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.complementEquiv line 144
  13. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.combined_compl line 166
  14. def OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient line 173
  15. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_reshuffle line 180
  16. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_gram line 200
  17. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.cfc_reindex line 212
  18. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_action_XY line 219
  19. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_action_Y line 226
  20. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_action_XP line 238
  21. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_action_P line 246
  22. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_reshuffle_gram line 258
  23. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMovePhysical.fourCoefficient_norm line 266