OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical235.lean

GitHub source file

156 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7520 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw7520step0 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw7520step1 line 15
  4. def OAI.MUB6.Certificate.PairSemantics.raw7520step2 line 17
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical7520 line 19
  6. def OAI.MUB6.Certificate.PairSemantics.raw7521 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw7521step0 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw7521step1 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw7521step2 line 42
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7521 line 44
  11. def OAI.MUB6.Certificate.PairSemantics.raw7522 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw7522step0 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw7522step1 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw7522step2 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7522 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw7523 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw7523step0 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw7523step1 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw7523step2 line 92
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7523 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw7524 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw7524step0 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7524step1 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7524 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw7525 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw7525step0 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw7525step1 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw7525step2 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7525 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw7526 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw7526step0 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw7526step1 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw7526step2 line 161
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7526 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw7527 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw7527step0 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw7527step1 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw7527step2 line 186
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7527 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw7528 line 205
  41. def OAI.MUB6.Certificate.PairSemantics.raw7528step0 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw7528step1 line 209
  43. def OAI.MUB6.Certificate.PairSemantics.raw7528step2 line 211
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7528 line 213
  45. def OAI.MUB6.Certificate.PairSemantics.raw7529 line 230
  46. def OAI.MUB6.Certificate.PairSemantics.raw7529step0 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw7529step1 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw7529step2 line 236
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7529 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw7530 line 255
  51. def OAI.MUB6.Certificate.PairSemantics.raw7530step0 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw7530step1 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw7530step2 line 261
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7530 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw7531 line 280
  56. def OAI.MUB6.Certificate.PairSemantics.raw7531step0 line 282
  57. def OAI.MUB6.Certificate.PairSemantics.raw7531step1 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw7531step2 line 286
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7531 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw7532 line 305
  61. def OAI.MUB6.Certificate.PairSemantics.raw7532step0 line 307
  62. def OAI.MUB6.Certificate.PairSemantics.raw7532step1 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw7532step2 line 311
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7532 line 313
  65. def OAI.MUB6.Certificate.PairSemantics.raw7533 line 330
  66. def OAI.MUB6.Certificate.PairSemantics.raw7533step0 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw7533step1 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw7533step2 line 336
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7533 line 338
  70. def OAI.MUB6.Certificate.PairSemantics.raw7534 line 355
  71. def OAI.MUB6.Certificate.PairSemantics.raw7534step0 line 357
  72. def OAI.MUB6.Certificate.PairSemantics.raw7534step1 line 359
  73. def OAI.MUB6.Certificate.PairSemantics.raw7534step2 line 361
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7534 line 363
  75. def OAI.MUB6.Certificate.PairSemantics.raw7535 line 380
  76. def OAI.MUB6.Certificate.PairSemantics.raw7535step0 line 382
  77. def OAI.MUB6.Certificate.PairSemantics.raw7535step1 line 384
  78. def OAI.MUB6.Certificate.PairSemantics.raw7535step2 line 386
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7535 line 388
  80. def OAI.MUB6.Certificate.PairSemantics.raw7536 line 405
  81. def OAI.MUB6.Certificate.PairSemantics.raw7536step0 line 407
  82. def OAI.MUB6.Certificate.PairSemantics.raw7536step1 line 409
  83. def OAI.MUB6.Certificate.PairSemantics.raw7536step2 line 411
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7536 line 413
  85. def OAI.MUB6.Certificate.PairSemantics.raw7537 line 430
  86. def OAI.MUB6.Certificate.PairSemantics.raw7537step0 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw7537step1 line 434
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7537 line 436
  89. def OAI.MUB6.Certificate.PairSemantics.raw7538 line 449
  90. def OAI.MUB6.Certificate.PairSemantics.raw7538step0 line 451
  91. def OAI.MUB6.Certificate.PairSemantics.raw7538step1 line 453
  92. def OAI.MUB6.Certificate.PairSemantics.raw7538step2 line 455
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7538 line 457
  94. def OAI.MUB6.Certificate.PairSemantics.raw7539 line 474
  95. def OAI.MUB6.Certificate.PairSemantics.raw7539step0 line 476
  96. def OAI.MUB6.Certificate.PairSemantics.raw7539step1 line 478
  97. def OAI.MUB6.Certificate.PairSemantics.raw7539step2 line 480
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7539 line 482
  99. def OAI.MUB6.Certificate.PairSemantics.raw7540 line 499
  100. def OAI.MUB6.Certificate.PairSemantics.raw7540step0 line 501
  101. def OAI.MUB6.Certificate.PairSemantics.raw7540step1 line 503
  102. def OAI.MUB6.Certificate.PairSemantics.raw7540step2 line 505
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7540 line 507
  104. def OAI.MUB6.Certificate.PairSemantics.raw7541 line 524
  105. def OAI.MUB6.Certificate.PairSemantics.raw7541step0 line 526
  106. def OAI.MUB6.Certificate.PairSemantics.raw7541step1 line 528
  107. def OAI.MUB6.Certificate.PairSemantics.raw7541step2 line 530
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7541 line 532
  109. def OAI.MUB6.Certificate.PairSemantics.raw7542 line 549
  110. def OAI.MUB6.Certificate.PairSemantics.raw7542step0 line 551
  111. def OAI.MUB6.Certificate.PairSemantics.raw7542step1 line 553
  112. def OAI.MUB6.Certificate.PairSemantics.raw7542step2 line 555
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7542 line 557
  114. def OAI.MUB6.Certificate.PairSemantics.raw7543 line 574
  115. def OAI.MUB6.Certificate.PairSemantics.raw7543step0 line 576
  116. def OAI.MUB6.Certificate.PairSemantics.raw7543step1 line 578
  117. def OAI.MUB6.Certificate.PairSemantics.raw7543step2 line 580
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7543 line 582
  119. def OAI.MUB6.Certificate.PairSemantics.raw7544 line 599
  120. def OAI.MUB6.Certificate.PairSemantics.raw7544step0 line 601
  121. def OAI.MUB6.Certificate.PairSemantics.raw7544step1 line 603
  122. def OAI.MUB6.Certificate.PairSemantics.raw7544step2 line 605
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical7544 line 607
  124. def OAI.MUB6.Certificate.PairSemantics.raw7545 line 624
  125. def OAI.MUB6.Certificate.PairSemantics.raw7545step0 line 626
  126. def OAI.MUB6.Certificate.PairSemantics.raw7545step1 line 628
  127. def OAI.MUB6.Certificate.PairSemantics.raw7545step2 line 630
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical7545 line 632
  129. def OAI.MUB6.Certificate.PairSemantics.raw7546 line 649
  130. def OAI.MUB6.Certificate.PairSemantics.raw7546step0 line 651
  131. def OAI.MUB6.Certificate.PairSemantics.raw7546step1 line 653
  132. def OAI.MUB6.Certificate.PairSemantics.raw7546step2 line 655
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical7546 line 657
  134. def OAI.MUB6.Certificate.PairSemantics.raw7547 line 674
  135. def OAI.MUB6.Certificate.PairSemantics.raw7547step0 line 676
  136. def OAI.MUB6.Certificate.PairSemantics.raw7547step1 line 678
  137. def OAI.MUB6.Certificate.PairSemantics.raw7547step2 line 680
  138. theorem OAI.MUB6.Certificate.PairSemantics.canonical7547 line 682
  139. def OAI.MUB6.Certificate.PairSemantics.raw7548 line 699
  140. def OAI.MUB6.Certificate.PairSemantics.raw7548step0 line 701
  141. def OAI.MUB6.Certificate.PairSemantics.raw7548step1 line 703
  142. def OAI.MUB6.Certificate.PairSemantics.raw7548step2 line 705
  143. theorem OAI.MUB6.Certificate.PairSemantics.canonical7548 line 707
  144. def OAI.MUB6.Certificate.PairSemantics.raw7549 line 724
  145. def OAI.MUB6.Certificate.PairSemantics.raw7549step0 line 726
  146. def OAI.MUB6.Certificate.PairSemantics.raw7549step1 line 728
  147. def OAI.MUB6.Certificate.PairSemantics.raw7549step2 line 730
  148. theorem OAI.MUB6.Certificate.PairSemantics.canonical7549 line 732
  149. def OAI.MUB6.Certificate.PairSemantics.raw7550 line 749
  150. def OAI.MUB6.Certificate.PairSemantics.raw7550step0 line 751
  151. def OAI.MUB6.Certificate.PairSemantics.raw7550step1 line 753
  152. def OAI.MUB6.Certificate.PairSemantics.raw7550step2 line 755
  153. theorem OAI.MUB6.Certificate.PairSemantics.canonical7550 line 757
  154. def OAI.MUB6.Certificate.PairSemantics.raw7551 line 774
  155. def OAI.MUB6.Certificate.PairSemantics.raw7551step0 line 776
  156. theorem OAI.MUB6.Certificate.PairSemantics.canonical7551 line 778