OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical131.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4192 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4192step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4192step1 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw4192step2 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4192 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw4193 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw4193step0 line 47
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4193 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw4194 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw4194step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw4194step1 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw4194step2 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4194 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw4195 line 83
  15. def OAI.MUB6.Certificate.PairSemantics.raw4195step0 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw4195step1 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw4195step2 line 89
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4195 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw4196 line 108
  20. def OAI.MUB6.Certificate.PairSemantics.raw4196step0 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw4196step1 line 112
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4196 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw4197 line 127
  24. def OAI.MUB6.Certificate.PairSemantics.raw4197step0 line 129
  25. def OAI.MUB6.Certificate.PairSemantics.raw4197step1 line 131
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4197 line 133
  27. def OAI.MUB6.Certificate.PairSemantics.raw4198 line 146
  28. def OAI.MUB6.Certificate.PairSemantics.raw4198step0 line 148
  29. def OAI.MUB6.Certificate.PairSemantics.raw4198step1 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw4198step2 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4198 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw4199 line 171
  33. def OAI.MUB6.Certificate.PairSemantics.raw4199step0 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw4199step1 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw4199step2 line 177
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4199 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw4200 line 196
  38. def OAI.MUB6.Certificate.PairSemantics.raw4200step0 line 198
  39. def OAI.MUB6.Certificate.PairSemantics.raw4200step1 line 200
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4200 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw4201 line 215
  42. def OAI.MUB6.Certificate.PairSemantics.raw4201step0 line 217
  43. def OAI.MUB6.Certificate.PairSemantics.raw4201step1 line 219
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4201 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw4202 line 234
  46. def OAI.MUB6.Certificate.PairSemantics.raw4202step0 line 236
  47. def OAI.MUB6.Certificate.PairSemantics.raw4202step1 line 238
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4202 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw4203 line 253
  50. def OAI.MUB6.Certificate.PairSemantics.raw4203step0 line 255
  51. def OAI.MUB6.Certificate.PairSemantics.raw4203step1 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw4203step2 line 259
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4203 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw4204 line 278
  55. def OAI.MUB6.Certificate.PairSemantics.raw4204step0 line 280
  56. def OAI.MUB6.Certificate.PairSemantics.raw4204step1 line 282
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4204 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw4205 line 297
  59. def OAI.MUB6.Certificate.PairSemantics.raw4205step0 line 299
  60. def OAI.MUB6.Certificate.PairSemantics.raw4205step1 line 301
  61. def OAI.MUB6.Certificate.PairSemantics.raw4205step2 line 303
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4205 line 305
  63. def OAI.MUB6.Certificate.PairSemantics.raw4206 line 322
  64. def OAI.MUB6.Certificate.PairSemantics.raw4206step0 line 324
  65. def OAI.MUB6.Certificate.PairSemantics.raw4206step1 line 326
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4206 line 328
  67. def OAI.MUB6.Certificate.PairSemantics.raw4207 line 341
  68. def OAI.MUB6.Certificate.PairSemantics.raw4207step0 line 343
  69. def OAI.MUB6.Certificate.PairSemantics.raw4207step1 line 345
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4207 line 347
  71. def OAI.MUB6.Certificate.PairSemantics.raw4208 line 360
  72. def OAI.MUB6.Certificate.PairSemantics.raw4208step0 line 362
  73. def OAI.MUB6.Certificate.PairSemantics.raw4208step1 line 364
  74. def OAI.MUB6.Certificate.PairSemantics.raw4208step2 line 366
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4208 line 368
  76. def OAI.MUB6.Certificate.PairSemantics.raw4209 line 385
  77. def OAI.MUB6.Certificate.PairSemantics.raw4209step0 line 387
  78. def OAI.MUB6.Certificate.PairSemantics.raw4209step1 line 389
  79. def OAI.MUB6.Certificate.PairSemantics.raw4209step2 line 391
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4209 line 393
  81. def OAI.MUB6.Certificate.PairSemantics.raw4210 line 410
  82. def OAI.MUB6.Certificate.PairSemantics.raw4210step0 line 412
  83. def OAI.MUB6.Certificate.PairSemantics.raw4210step1 line 414
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4210 line 416
  85. def OAI.MUB6.Certificate.PairSemantics.raw4211 line 429
  86. def OAI.MUB6.Certificate.PairSemantics.raw4211step0 line 431
  87. def OAI.MUB6.Certificate.PairSemantics.raw4211step1 line 433
  88. def OAI.MUB6.Certificate.PairSemantics.raw4211step2 line 435
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4211 line 437
  90. def OAI.MUB6.Certificate.PairSemantics.raw4212 line 454
  91. def OAI.MUB6.Certificate.PairSemantics.raw4212step0 line 456
  92. def OAI.MUB6.Certificate.PairSemantics.raw4212step1 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw4212step2 line 460
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4212 line 462
  95. def OAI.MUB6.Certificate.PairSemantics.raw4213 line 479
  96. def OAI.MUB6.Certificate.PairSemantics.raw4213step0 line 481
  97. def OAI.MUB6.Certificate.PairSemantics.raw4213step1 line 483
  98. def OAI.MUB6.Certificate.PairSemantics.raw4213step2 line 485
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical4213 line 487
  100. def OAI.MUB6.Certificate.PairSemantics.raw4214 line 504
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4214 line 506
  102. def OAI.MUB6.Certificate.PairSemantics.raw4215 line 510
  103. def OAI.MUB6.Certificate.PairSemantics.raw4215step0 line 512
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4215 line 514
  105. def OAI.MUB6.Certificate.PairSemantics.raw4216 line 523
  106. def OAI.MUB6.Certificate.PairSemantics.raw4216step0 line 525
  107. def OAI.MUB6.Certificate.PairSemantics.raw4216step1 line 527
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4216 line 529
  109. def OAI.MUB6.Certificate.PairSemantics.raw4217 line 542
  110. def OAI.MUB6.Certificate.PairSemantics.raw4217step0 line 544
  111. def OAI.MUB6.Certificate.PairSemantics.raw4217step1 line 546
  112. def OAI.MUB6.Certificate.PairSemantics.raw4217step2 line 548
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical4217 line 550
  114. def OAI.MUB6.Certificate.PairSemantics.raw4218 line 567
  115. def OAI.MUB6.Certificate.PairSemantics.raw4218step0 line 569
  116. def OAI.MUB6.Certificate.PairSemantics.raw4218step1 line 571
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical4218 line 573
  118. def OAI.MUB6.Certificate.PairSemantics.raw4219 line 586
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical4219 line 588
  120. def OAI.MUB6.Certificate.PairSemantics.raw4220 line 592
  121. def OAI.MUB6.Certificate.PairSemantics.raw4220step0 line 594
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical4220 line 596
  123. def OAI.MUB6.Certificate.PairSemantics.raw4221 line 605
  124. def OAI.MUB6.Certificate.PairSemantics.raw4221step0 line 607
  125. def OAI.MUB6.Certificate.PairSemantics.raw4221step1 line 609
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical4221 line 611
  127. def OAI.MUB6.Certificate.PairSemantics.raw4222 line 624
  128. def OAI.MUB6.Certificate.PairSemantics.raw4222step0 line 626
  129. def OAI.MUB6.Certificate.PairSemantics.raw4222step1 line 628
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical4222 line 630
  131. def OAI.MUB6.Certificate.PairSemantics.raw4223 line 643
  132. def OAI.MUB6.Certificate.PairSemantics.raw4223step0 line 645
  133. def OAI.MUB6.Certificate.PairSemantics.raw4223step1 line 647
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical4223 line 649