OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical180.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5760 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw5760step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw5760step1 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw5760step2 line 22
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5760 line 24
  6. def OAI.MUB6.Certificate.PairSemantics.raw5761 line 42
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical5761 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw5762 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5762 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw5763 line 54
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5763 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw5764 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5764 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw5765 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw5765step0 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw5765step1 line 70
  17. def OAI.MUB6.Certificate.PairSemantics.raw5765step2 line 72
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical5765 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw5766 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw5766step0 line 93
  21. def OAI.MUB6.Certificate.PairSemantics.raw5766step1 line 95
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5766 line 97
  23. def OAI.MUB6.Certificate.PairSemantics.raw5767 line 110
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5767 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw5768 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw5768step0 line 118
  27. def OAI.MUB6.Certificate.PairSemantics.raw5768step1 line 120
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5768 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw5769 line 135
  30. def OAI.MUB6.Certificate.PairSemantics.raw5769step0 line 137
  31. def OAI.MUB6.Certificate.PairSemantics.raw5769step1 line 139
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5769 line 141
  33. def OAI.MUB6.Certificate.PairSemantics.raw5770 line 154
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical5770 line 156
  35. def OAI.MUB6.Certificate.PairSemantics.raw5771 line 160
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5771 line 162
  37. def OAI.MUB6.Certificate.PairSemantics.raw5772 line 166
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5772 line 168
  39. def OAI.MUB6.Certificate.PairSemantics.raw5773 line 172
  40. def OAI.MUB6.Certificate.PairSemantics.raw5773step0 line 174
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5773 line 176
  42. def OAI.MUB6.Certificate.PairSemantics.raw5774 line 185
  43. def OAI.MUB6.Certificate.PairSemantics.raw5774step0 line 187
  44. def OAI.MUB6.Certificate.PairSemantics.raw5774step1 line 189
  45. def OAI.MUB6.Certificate.PairSemantics.raw5774step2 line 191
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5774 line 193
  47. def OAI.MUB6.Certificate.PairSemantics.raw5775 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw5775step0 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw5775step1 line 214
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical5775 line 216
  51. def OAI.MUB6.Certificate.PairSemantics.raw5776 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw5776step0 line 231
  53. def OAI.MUB6.Certificate.PairSemantics.raw5776step1 line 233
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5776 line 235
  55. def OAI.MUB6.Certificate.PairSemantics.raw5777 line 248
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5777 line 250
  57. def OAI.MUB6.Certificate.PairSemantics.raw5778 line 254
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5778 line 256
  59. def OAI.MUB6.Certificate.PairSemantics.raw5779 line 260
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5779 line 262
  61. def OAI.MUB6.Certificate.PairSemantics.raw5780 line 266
  62. def OAI.MUB6.Certificate.PairSemantics.raw5780step0 line 268
  63. def OAI.MUB6.Certificate.PairSemantics.raw5780step1 line 270
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5780 line 272
  65. def OAI.MUB6.Certificate.PairSemantics.raw5781 line 285
  66. def OAI.MUB6.Certificate.PairSemantics.raw5781step0 line 287
  67. def OAI.MUB6.Certificate.PairSemantics.raw5781step1 line 289
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5781 line 291
  69. def OAI.MUB6.Certificate.PairSemantics.raw5782 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw5782step0 line 306
  71. def OAI.MUB6.Certificate.PairSemantics.raw5782step1 line 308
  72. def OAI.MUB6.Certificate.PairSemantics.raw5782step2 line 310
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5782 line 312
  74. def OAI.MUB6.Certificate.PairSemantics.raw5783 line 329
  75. def OAI.MUB6.Certificate.PairSemantics.raw5783step0 line 331
  76. def OAI.MUB6.Certificate.PairSemantics.raw5783step1 line 333
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5783 line 335
  78. def OAI.MUB6.Certificate.PairSemantics.raw5784 line 348
  79. def OAI.MUB6.Certificate.PairSemantics.raw5784step0 line 350
  80. def OAI.MUB6.Certificate.PairSemantics.raw5784step1 line 352
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5784 line 354
  82. def OAI.MUB6.Certificate.PairSemantics.raw5785 line 367
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5785 line 369
  84. def OAI.MUB6.Certificate.PairSemantics.raw5786 line 373
  85. def OAI.MUB6.Certificate.PairSemantics.raw5786step0 line 375
  86. def OAI.MUB6.Certificate.PairSemantics.raw5786step1 line 377
  87. def OAI.MUB6.Certificate.PairSemantics.raw5786step2 line 379
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5786 line 381
  89. def OAI.MUB6.Certificate.PairSemantics.raw5787 line 398
  90. def OAI.MUB6.Certificate.PairSemantics.raw5787step0 line 400
  91. def OAI.MUB6.Certificate.PairSemantics.raw5787step1 line 402
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical5787 line 404
  93. def OAI.MUB6.Certificate.PairSemantics.raw5788 line 417
  94. def OAI.MUB6.Certificate.PairSemantics.raw5788step0 line 419
  95. def OAI.MUB6.Certificate.PairSemantics.raw5788step1 line 421
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical5788 line 423
  97. def OAI.MUB6.Certificate.PairSemantics.raw5789 line 436
  98. def OAI.MUB6.Certificate.PairSemantics.raw5789step0 line 438
  99. def OAI.MUB6.Certificate.PairSemantics.raw5789step1 line 440
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical5789 line 442
  101. def OAI.MUB6.Certificate.PairSemantics.raw5790 line 455
  102. def OAI.MUB6.Certificate.PairSemantics.raw5790step0 line 457
  103. def OAI.MUB6.Certificate.PairSemantics.raw5790step1 line 459
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical5790 line 461
  105. def OAI.MUB6.Certificate.PairSemantics.raw5791 line 474
  106. def OAI.MUB6.Certificate.PairSemantics.raw5791step0 line 476
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical5791 line 478