OAI/Analysis/Quantum/PPTSquare/Commutators.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PencilAlgebra.N0_N1_row0 line 9
  2. lemma OAI.PencilAlgebra.N0_N1_row1 line 10
  3. lemma OAI.PencilAlgebra.N0_N1_row2 line 11
  4. lemma OAI.PencilAlgebra.N0_N1_row3 line 12
  5. lemma OAI.PencilAlgebra.N0_N1_row4 line 13
  6. lemma OAI.PencilAlgebra.N0_N1_row5 line 14
  7. lemma OAI.PencilAlgebra.N0_N1_row6 line 15
  8. lemma OAI.PencilAlgebra.N0_N1_row7 line 16
  9. lemma OAI.PencilAlgebra.N0_N1_row8 line 17
  10. lemma OAI.PencilAlgebra.N0_N1_row9 line 18
  11. lemma OAI.PencilAlgebra.N0_N1_row10 line 19
  12. lemma OAI.PencilAlgebra.N0_N1_row11 line 20
  13. lemma OAI.PencilAlgebra.N0_N1_row12 line 21
  14. lemma OAI.PencilAlgebra.N0_N1_row13 line 22
  15. lemma OAI.PencilAlgebra.N0_N1_row14 line 23
  16. lemma OAI.PencilAlgebra.N0_N1_row15 line 24
  17. lemma OAI.PencilAlgebra.N0_N1_row16 line 25
  18. lemma OAI.PencilAlgebra.N0_N1_row17 line 26
  19. lemma OAI.PencilAlgebra.N0_N1_row18 line 27
  20. lemma OAI.PencilAlgebra.N0_N1_row19 line 28
  21. lemma OAI.PencilAlgebra.N0_N1 line 29
  22. lemma OAI.PencilAlgebra.N0_N2_row0 line 52
  23. lemma OAI.PencilAlgebra.N0_N2_row1 line 53
  24. lemma OAI.PencilAlgebra.N0_N2_row2 line 54
  25. lemma OAI.PencilAlgebra.N0_N2_row3 line 55
  26. lemma OAI.PencilAlgebra.N0_N2_row4 line 56
  27. lemma OAI.PencilAlgebra.N0_N2_row5 line 57
  28. lemma OAI.PencilAlgebra.N0_N2_row6 line 58
  29. lemma OAI.PencilAlgebra.N0_N2_row7 line 59
  30. lemma OAI.PencilAlgebra.N0_N2_row8 line 60
  31. lemma OAI.PencilAlgebra.N0_N2_row9 line 61
  32. lemma OAI.PencilAlgebra.N0_N2_row10 line 62
  33. lemma OAI.PencilAlgebra.N0_N2_row11 line 63
  34. lemma OAI.PencilAlgebra.N0_N2_row12 line 64
  35. lemma OAI.PencilAlgebra.N0_N2_row13 line 65
  36. lemma OAI.PencilAlgebra.N0_N2_row14 line 66
  37. lemma OAI.PencilAlgebra.N0_N2_row15 line 67
  38. lemma OAI.PencilAlgebra.N0_N2_row16 line 68
  39. lemma OAI.PencilAlgebra.N0_N2_row17 line 69
  40. lemma OAI.PencilAlgebra.N0_N2_row18 line 70
  41. lemma OAI.PencilAlgebra.N0_N2_row19 line 71
  42. lemma OAI.PencilAlgebra.N0_N2 line 72
  43. lemma OAI.PencilAlgebra.N1_N2_row0 line 95
  44. lemma OAI.PencilAlgebra.N1_N2_row1 line 96
  45. lemma OAI.PencilAlgebra.N1_N2_row2 line 97
  46. lemma OAI.PencilAlgebra.N1_N2_row3 line 98
  47. lemma OAI.PencilAlgebra.N1_N2_row4 line 99
  48. lemma OAI.PencilAlgebra.N1_N2_row5 line 100
  49. lemma OAI.PencilAlgebra.N1_N2_row6 line 101
  50. lemma OAI.PencilAlgebra.N1_N2_row7 line 102
  51. lemma OAI.PencilAlgebra.N1_N2_row8 line 103
  52. lemma OAI.PencilAlgebra.N1_N2_row9 line 104
  53. lemma OAI.PencilAlgebra.N1_N2_row10 line 105
  54. lemma OAI.PencilAlgebra.N1_N2_row11 line 106
  55. lemma OAI.PencilAlgebra.N1_N2_row12 line 107
  56. lemma OAI.PencilAlgebra.N1_N2_row13 line 108
  57. lemma OAI.PencilAlgebra.N1_N2_row14 line 109
  58. lemma OAI.PencilAlgebra.N1_N2_row15 line 110
  59. lemma OAI.PencilAlgebra.N1_N2_row16 line 111
  60. lemma OAI.PencilAlgebra.N1_N2_row17 line 112
  61. lemma OAI.PencilAlgebra.N1_N2_row18 line 113
  62. lemma OAI.PencilAlgebra.N1_N2_row19 line 114
  63. lemma OAI.PencilAlgebra.N1_N2 line 115