OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical316.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10112 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw10112step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw10112step1 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical10112 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw10113 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw10113step0 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical10113 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw10114 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw10114step0 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical10114 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw10115 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw10115step0 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw10115step1 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw10115step2 line 64
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical10115 line 66
  16. def OAI.MUB6.Certificate.PairSemantics.raw10116 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw10116step0 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw10116step1 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw10116step2 line 89
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical10116 line 91
  21. def OAI.MUB6.Certificate.PairSemantics.raw10117 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw10117step0 line 110
  23. def OAI.MUB6.Certificate.PairSemantics.raw10117step1 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw10117step2 line 114
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical10117 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw10118 line 133
  27. def OAI.MUB6.Certificate.PairSemantics.raw10118step0 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw10118step1 line 137
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical10118 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw10119 line 152
  31. def OAI.MUB6.Certificate.PairSemantics.raw10119step0 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw10119step1 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw10119step2 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical10119 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw10120 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw10120step0 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw10120step1 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw10120step2 line 183
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical10120 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw10121 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw10121step0 line 204
  42. def OAI.MUB6.Certificate.PairSemantics.raw10121step1 line 206
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical10121 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw10122 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw10122step0 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw10122step1 line 225
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical10122 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw10123 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw10123step0 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw10123step1 line 244
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical10123 line 246
  52. def OAI.MUB6.Certificate.PairSemantics.raw10124 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw10124step0 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw10124step1 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw10124step2 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical10124 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw10125 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw10125step0 line 286
  59. def OAI.MUB6.Certificate.PairSemantics.raw10125step1 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw10125step2 line 290
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical10125 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw10126 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw10126step0 line 311
  64. def OAI.MUB6.Certificate.PairSemantics.raw10126step1 line 313
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical10126 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw10127 line 328
  67. def OAI.MUB6.Certificate.PairSemantics.raw10127step0 line 330
  68. def OAI.MUB6.Certificate.PairSemantics.raw10127step1 line 332
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical10127 line 334
  70. def OAI.MUB6.Certificate.PairSemantics.raw10128 line 347
  71. def OAI.MUB6.Certificate.PairSemantics.raw10128step0 line 349
  72. def OAI.MUB6.Certificate.PairSemantics.raw10128step1 line 351
  73. def OAI.MUB6.Certificate.PairSemantics.raw10128step2 line 353
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical10128 line 355
  75. def OAI.MUB6.Certificate.PairSemantics.raw10129 line 372
  76. def OAI.MUB6.Certificate.PairSemantics.raw10129step0 line 374
  77. def OAI.MUB6.Certificate.PairSemantics.raw10129step1 line 376
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical10129 line 378
  79. def OAI.MUB6.Certificate.PairSemantics.raw10130 line 391
  80. def OAI.MUB6.Certificate.PairSemantics.raw10130step0 line 393
  81. def OAI.MUB6.Certificate.PairSemantics.raw10130step1 line 395
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical10130 line 397
  83. def OAI.MUB6.Certificate.PairSemantics.raw10131 line 410
  84. def OAI.MUB6.Certificate.PairSemantics.raw10131step0 line 412
  85. def OAI.MUB6.Certificate.PairSemantics.raw10131step1 line 414
  86. def OAI.MUB6.Certificate.PairSemantics.raw10131step2 line 416
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical10131 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw10132 line 435
  89. def OAI.MUB6.Certificate.PairSemantics.raw10132step0 line 437
  90. def OAI.MUB6.Certificate.PairSemantics.raw10132step1 line 439
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical10132 line 441
  92. def OAI.MUB6.Certificate.PairSemantics.raw10133 line 454
  93. def OAI.MUB6.Certificate.PairSemantics.raw10133step0 line 456
  94. def OAI.MUB6.Certificate.PairSemantics.raw10133step1 line 458
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical10133 line 460
  96. def OAI.MUB6.Certificate.PairSemantics.raw10134 line 473
  97. def OAI.MUB6.Certificate.PairSemantics.raw10134step0 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw10134step1 line 477
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical10134 line 479
  100. def OAI.MUB6.Certificate.PairSemantics.raw10135 line 492
  101. def OAI.MUB6.Certificate.PairSemantics.raw10135step0 line 494
  102. def OAI.MUB6.Certificate.PairSemantics.raw10135step1 line 496
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical10135 line 498
  104. def OAI.MUB6.Certificate.PairSemantics.raw10136 line 511
  105. def OAI.MUB6.Certificate.PairSemantics.raw10136step0 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw10136step1 line 515
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical10136 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw10137 line 530
  109. def OAI.MUB6.Certificate.PairSemantics.raw10137step0 line 532
  110. def OAI.MUB6.Certificate.PairSemantics.raw10137step1 line 534
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical10137 line 536
  112. def OAI.MUB6.Certificate.PairSemantics.raw10138 line 549
  113. def OAI.MUB6.Certificate.PairSemantics.raw10138step0 line 551
  114. def OAI.MUB6.Certificate.PairSemantics.raw10138step1 line 553
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical10138 line 555
  116. def OAI.MUB6.Certificate.PairSemantics.raw10139 line 568
  117. def OAI.MUB6.Certificate.PairSemantics.raw10139step0 line 570
  118. def OAI.MUB6.Certificate.PairSemantics.raw10139step1 line 572
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical10139 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw10140 line 587
  121. def OAI.MUB6.Certificate.PairSemantics.raw10140step0 line 589
  122. def OAI.MUB6.Certificate.PairSemantics.raw10140step1 line 591
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical10140 line 593
  124. def OAI.MUB6.Certificate.PairSemantics.raw10141 line 606
  125. def OAI.MUB6.Certificate.PairSemantics.raw10141step0 line 608
  126. def OAI.MUB6.Certificate.PairSemantics.raw10141step1 line 610
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical10141 line 612
  128. def OAI.MUB6.Certificate.PairSemantics.raw10142 line 625
  129. def OAI.MUB6.Certificate.PairSemantics.raw10142step0 line 627
  130. def OAI.MUB6.Certificate.PairSemantics.raw10142step1 line 629
  131. theorem OAI.MUB6.Certificate.PairSemantics.canonical10142 line 631
  132. def OAI.MUB6.Certificate.PairSemantics.raw10143 line 644
  133. def OAI.MUB6.Certificate.PairSemantics.raw10143step0 line 646
  134. def OAI.MUB6.Certificate.PairSemantics.raw10143step1 line 648
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical10143 line 650