OAI/Analysis/JiangSu/MatrixAlgebras/MatrixPartialFlips.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixTensor.Four line 15
  2. def OAI.MatrixTensor.swapP line 17
  3. def OAI.MatrixTensor.swapQ line 23
  4. def OAI.MatrixTensor.partialP line 29
  5. def OAI.MatrixTensor.partialQ line 30
  6. lemma OAI.MatrixTensor.partialP_sq line 32
  7. lemma OAI.MatrixTensor.partialQ_sq line 36
  8. lemma OAI.MatrixTensor.partial_commute line 40
  9. lemma OAI.MatrixTensor.partial_product line 44
  10. lemma OAI.MatrixTensor.partial_flip line 49
  11. def OAI.MatrixTensor.entryHom line 54
  12. lemma OAI.MatrixTensor.partialP_expansion line 59
  13. lemma OAI.MatrixTensor.partialQ_expansion line 72
  14. lemma OAI.MatrixTensor.partialP_mem line 85
  15. lemma OAI.MatrixTensor.partialQ_mem line 90
  16. lemma OAI.MatrixTensor.partialQ_conjugate_right_tensor line 96
  17. lemma OAI.MatrixTensor.partialP_conjugate_right_tensor line 109
  18. lemma OAI.MatrixTensor.partialP_star line 134
  19. lemma OAI.MatrixTensor.partialQ_star line 137
  20. lemma OAI.MatrixTensor.partialQ_conjugate_right_mem line 141
  21. lemma OAI.MatrixTensor.partialP_conjugate_right_mem line 152
  22. def OAI.MatrixTensor.pFlow line 164
  23. def OAI.MatrixTensor.qFlow line 166
  24. lemma OAI.MatrixTensor.pFlow_continuous line 168
  25. lemma OAI.MatrixTensor.qFlow_continuous line 169
  26. lemma OAI.MatrixTensor.pFlow_one line 170
  27. lemma OAI.MatrixTensor.qFlow_one line 172
  28. lemma OAI.MatrixTensor.flows_commute line 174
  29. lemma OAI.MatrixTensor.pFlow_mem line 176
  30. lemma OAI.MatrixTensor.qFlow_mem line 179
  31. lemma OAI.MatrixTensor.pFlow_period line 182
  32. lemma OAI.MatrixTensor.qFlow_period line 184