OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical35.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1120 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw1120step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw1120step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1120 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw1121 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw1121step0 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw1121step1 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw1121step2 line 39
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1121 line 41
  10. def OAI.MUB6.Certificate.PairSemantics.raw1122 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1122 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw1123 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw1123step0 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw1123step1 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1123 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw1124 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw1124step0 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw1124step1 line 87
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1124 line 89
  20. def OAI.MUB6.Certificate.PairSemantics.raw1125 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw1125step0 line 104
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1125 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw1126 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw1126step0 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw1126step1 line 119
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1126 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw1127 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw1127step0 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1127 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw1128 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw1128step0 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw1128step1 line 151
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1128 line 153
  34. def OAI.MUB6.Certificate.PairSemantics.raw1129 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw1129step0 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw1129step1 line 170
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1129 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw1130 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw1130step0 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw1130step1 line 189
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1130 line 191
  42. def OAI.MUB6.Certificate.PairSemantics.raw1131 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw1131step0 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw1131step1 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw1131step2 line 210
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1131 line 212
  47. def OAI.MUB6.Certificate.PairSemantics.raw1132 line 229
  48. def OAI.MUB6.Certificate.PairSemantics.raw1132step0 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw1132step1 line 233
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1132 line 235
  51. def OAI.MUB6.Certificate.PairSemantics.raw1133 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw1133step0 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw1133step1 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw1133step2 line 254
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1133 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw1134 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw1134step0 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw1134step1 line 277
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1134 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw1135 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw1135step0 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw1135step1 line 296
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1135 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw1136 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw1136step0 line 313
  66. def OAI.MUB6.Certificate.PairSemantics.raw1136step1 line 315
  67. def OAI.MUB6.Certificate.PairSemantics.raw1136step2 line 317
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1136 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw1137 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw1137step0 line 338
  71. def OAI.MUB6.Certificate.PairSemantics.raw1137step1 line 340
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1137 line 342
  73. def OAI.MUB6.Certificate.PairSemantics.raw1138 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw1138step0 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw1138step1 line 359
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1138 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw1139 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw1139step0 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw1139step1 line 378
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1139 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw1140 line 393
  82. def OAI.MUB6.Certificate.PairSemantics.raw1140step0 line 395
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1140 line 397
  84. def OAI.MUB6.Certificate.PairSemantics.raw1141 line 406
  85. def OAI.MUB6.Certificate.PairSemantics.raw1141step0 line 408
  86. def OAI.MUB6.Certificate.PairSemantics.raw1141step1 line 410
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1141 line 412
  88. def OAI.MUB6.Certificate.PairSemantics.raw1142 line 425
  89. def OAI.MUB6.Certificate.PairSemantics.raw1142step0 line 427
  90. def OAI.MUB6.Certificate.PairSemantics.raw1142step1 line 429
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical1142 line 431
  92. def OAI.MUB6.Certificate.PairSemantics.raw1143 line 444
  93. def OAI.MUB6.Certificate.PairSemantics.raw1143step0 line 446
  94. def OAI.MUB6.Certificate.PairSemantics.raw1143step1 line 448
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical1143 line 450
  96. def OAI.MUB6.Certificate.PairSemantics.raw1144 line 463
  97. def OAI.MUB6.Certificate.PairSemantics.raw1144step0 line 465
  98. def OAI.MUB6.Certificate.PairSemantics.raw1144step1 line 467
  99. def OAI.MUB6.Certificate.PairSemantics.raw1144step2 line 469
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical1144 line 471
  101. def OAI.MUB6.Certificate.PairSemantics.raw1145 line 488
  102. def OAI.MUB6.Certificate.PairSemantics.raw1145step0 line 490
  103. def OAI.MUB6.Certificate.PairSemantics.raw1145step1 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw1145step2 line 494
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1145 line 496
  106. def OAI.MUB6.Certificate.PairSemantics.raw1146 line 513
  107. def OAI.MUB6.Certificate.PairSemantics.raw1146step0 line 515
  108. def OAI.MUB6.Certificate.PairSemantics.raw1146step1 line 517
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical1146 line 519
  110. def OAI.MUB6.Certificate.PairSemantics.raw1147 line 532
  111. def OAI.MUB6.Certificate.PairSemantics.raw1147step0 line 534
  112. def OAI.MUB6.Certificate.PairSemantics.raw1147step1 line 536
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical1147 line 538
  114. def OAI.MUB6.Certificate.PairSemantics.raw1148 line 551
  115. def OAI.MUB6.Certificate.PairSemantics.raw1148step0 line 553
  116. def OAI.MUB6.Certificate.PairSemantics.raw1148step1 line 555
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical1148 line 557
  118. def OAI.MUB6.Certificate.PairSemantics.raw1149 line 570
  119. def OAI.MUB6.Certificate.PairSemantics.raw1149step0 line 572
  120. def OAI.MUB6.Certificate.PairSemantics.raw1149step1 line 574
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical1149 line 576
  122. def OAI.MUB6.Certificate.PairSemantics.raw1150 line 589
  123. def OAI.MUB6.Certificate.PairSemantics.raw1150step0 line 591
  124. def OAI.MUB6.Certificate.PairSemantics.raw1150step1 line 593
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical1150 line 595
  126. def OAI.MUB6.Certificate.PairSemantics.raw1151 line 608
  127. def OAI.MUB6.Certificate.PairSemantics.raw1151step0 line 610
  128. def OAI.MUB6.Certificate.PairSemantics.raw1151step1 line 612
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical1151 line 614