OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical283.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9056 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw9056step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw9056step1 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw9056step2 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw9056step3 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw9056step4 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw9056step5 line 29
  8. def OAI.MUB6.Certificate.PairSemantics.raw9056step6 line 31
  9. def OAI.MUB6.Certificate.PairSemantics.raw9056step7 line 33
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9056 line 35
  11. def OAI.MUB6.Certificate.PairSemantics.raw9057 line 80
  12. def OAI.MUB6.Certificate.PairSemantics.raw9057step0 line 82
  13. def OAI.MUB6.Certificate.PairSemantics.raw9057step1 line 84
  14. def OAI.MUB6.Certificate.PairSemantics.raw9057step2 line 86
  15. def OAI.MUB6.Certificate.PairSemantics.raw9057step3 line 88
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9057 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw9058 line 114
  18. def OAI.MUB6.Certificate.PairSemantics.raw9058step0 line 116
  19. def OAI.MUB6.Certificate.PairSemantics.raw9058step1 line 118
  20. def OAI.MUB6.Certificate.PairSemantics.raw9058step2 line 120
  21. def OAI.MUB6.Certificate.PairSemantics.raw9058step3 line 122
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9058 line 124
  23. def OAI.MUB6.Certificate.PairSemantics.raw9059 line 148
  24. def OAI.MUB6.Certificate.PairSemantics.raw9059step0 line 150
  25. def OAI.MUB6.Certificate.PairSemantics.raw9059step1 line 152
  26. def OAI.MUB6.Certificate.PairSemantics.raw9059step2 line 154
  27. def OAI.MUB6.Certificate.PairSemantics.raw9059step3 line 156
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9059 line 158
  29. def OAI.MUB6.Certificate.PairSemantics.raw9060 line 182
  30. def OAI.MUB6.Certificate.PairSemantics.raw9060step0 line 184
  31. def OAI.MUB6.Certificate.PairSemantics.raw9060step1 line 186
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9060 line 188
  33. def OAI.MUB6.Certificate.PairSemantics.raw9061 line 202
  34. def OAI.MUB6.Certificate.PairSemantics.raw9061step0 line 204
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9061 line 206
  36. def OAI.MUB6.Certificate.PairSemantics.raw9062 line 215
  37. def OAI.MUB6.Certificate.PairSemantics.raw9062step0 line 217
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9062 line 219
  39. def OAI.MUB6.Certificate.PairSemantics.raw9063 line 228
  40. def OAI.MUB6.Certificate.PairSemantics.raw9063step0 line 230
  41. def OAI.MUB6.Certificate.PairSemantics.raw9063step1 line 232
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9063 line 234
  43. def OAI.MUB6.Certificate.PairSemantics.raw9064 line 247
  44. def OAI.MUB6.Certificate.PairSemantics.raw9064step0 line 249
  45. def OAI.MUB6.Certificate.PairSemantics.raw9064step1 line 251
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9064 line 253
  47. def OAI.MUB6.Certificate.PairSemantics.raw9065 line 266
  48. def OAI.MUB6.Certificate.PairSemantics.raw9065step0 line 268
  49. def OAI.MUB6.Certificate.PairSemantics.raw9065step1 line 270
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9065 line 272
  51. def OAI.MUB6.Certificate.PairSemantics.raw9066 line 285
  52. def OAI.MUB6.Certificate.PairSemantics.raw9066step0 line 287
  53. def OAI.MUB6.Certificate.PairSemantics.raw9066step1 line 289
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9066 line 291
  55. def OAI.MUB6.Certificate.PairSemantics.raw9067 line 304
  56. def OAI.MUB6.Certificate.PairSemantics.raw9067step0 line 306
  57. def OAI.MUB6.Certificate.PairSemantics.raw9067step1 line 308
  58. def OAI.MUB6.Certificate.PairSemantics.raw9067step2 line 310
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9067 line 312
  60. def OAI.MUB6.Certificate.PairSemantics.raw9068 line 330
  61. def OAI.MUB6.Certificate.PairSemantics.raw9068step0 line 332
  62. def OAI.MUB6.Certificate.PairSemantics.raw9068step1 line 334
  63. def OAI.MUB6.Certificate.PairSemantics.raw9068step2 line 336
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical9068 line 338
  65. def OAI.MUB6.Certificate.PairSemantics.raw9069 line 356
  66. def OAI.MUB6.Certificate.PairSemantics.raw9069step0 line 358
  67. def OAI.MUB6.Certificate.PairSemantics.raw9069step1 line 360
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9069 line 362
  69. def OAI.MUB6.Certificate.PairSemantics.raw9070 line 376
  70. def OAI.MUB6.Certificate.PairSemantics.raw9070step0 line 378
  71. def OAI.MUB6.Certificate.PairSemantics.raw9070step1 line 380
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9070 line 382
  73. def OAI.MUB6.Certificate.PairSemantics.raw9071 line 396
  74. def OAI.MUB6.Certificate.PairSemantics.raw9071step0 line 398
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9071 line 400
  76. def OAI.MUB6.Certificate.PairSemantics.raw9072 line 409
  77. def OAI.MUB6.Certificate.PairSemantics.raw9072step0 line 411
  78. def OAI.MUB6.Certificate.PairSemantics.raw9072step1 line 413
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9072 line 415
  80. def OAI.MUB6.Certificate.PairSemantics.raw9073 line 428
  81. def OAI.MUB6.Certificate.PairSemantics.raw9073step0 line 430
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9073 line 432
  83. def OAI.MUB6.Certificate.PairSemantics.raw9074 line 441
  84. def OAI.MUB6.Certificate.PairSemantics.raw9074step0 line 443
  85. def OAI.MUB6.Certificate.PairSemantics.raw9074step1 line 445
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9074 line 447
  87. def OAI.MUB6.Certificate.PairSemantics.raw9075 line 461
  88. def OAI.MUB6.Certificate.PairSemantics.raw9075step0 line 463
  89. def OAI.MUB6.Certificate.PairSemantics.raw9075step1 line 465
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9075 line 467
  91. def OAI.MUB6.Certificate.PairSemantics.raw9076 line 481
  92. def OAI.MUB6.Certificate.PairSemantics.raw9076step0 line 483
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9076 line 485
  94. def OAI.MUB6.Certificate.PairSemantics.raw9077 line 494
  95. def OAI.MUB6.Certificate.PairSemantics.raw9077step0 line 496
  96. def OAI.MUB6.Certificate.PairSemantics.raw9077step1 line 498
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9077 line 500
  98. def OAI.MUB6.Certificate.PairSemantics.raw9078 line 514
  99. def OAI.MUB6.Certificate.PairSemantics.raw9078step0 line 516
  100. def OAI.MUB6.Certificate.PairSemantics.raw9078step1 line 518
  101. def OAI.MUB6.Certificate.PairSemantics.raw9078step2 line 520
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9078 line 522
  103. def OAI.MUB6.Certificate.PairSemantics.raw9079 line 540
  104. def OAI.MUB6.Certificate.PairSemantics.raw9079step0 line 542
  105. def OAI.MUB6.Certificate.PairSemantics.raw9079step1 line 544
  106. def OAI.MUB6.Certificate.PairSemantics.raw9079step2 line 546
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9079 line 548
  108. def OAI.MUB6.Certificate.PairSemantics.raw9080 line 566
  109. def OAI.MUB6.Certificate.PairSemantics.raw9080step0 line 568
  110. def OAI.MUB6.Certificate.PairSemantics.raw9080step1 line 570
  111. def OAI.MUB6.Certificate.PairSemantics.raw9080step2 line 572
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical9080 line 574
  113. def OAI.MUB6.Certificate.PairSemantics.raw9081 line 592
  114. def OAI.MUB6.Certificate.PairSemantics.raw9081step0 line 594
  115. def OAI.MUB6.Certificate.PairSemantics.raw9081step1 line 596
  116. def OAI.MUB6.Certificate.PairSemantics.raw9081step2 line 598
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical9081 line 600
  118. def OAI.MUB6.Certificate.PairSemantics.raw9082 line 617
  119. def OAI.MUB6.Certificate.PairSemantics.raw9082step0 line 619
  120. def OAI.MUB6.Certificate.PairSemantics.raw9082step1 line 621
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical9082 line 623
  122. def OAI.MUB6.Certificate.PairSemantics.raw9083 line 636
  123. def OAI.MUB6.Certificate.PairSemantics.raw9083step0 line 638
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical9083 line 640
  125. def OAI.MUB6.Certificate.PairSemantics.raw9084 line 649
  126. def OAI.MUB6.Certificate.PairSemantics.raw9084step0 line 651
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical9084 line 653
  128. def OAI.MUB6.Certificate.PairSemantics.raw9085 line 662
  129. def OAI.MUB6.Certificate.PairSemantics.raw9085step0 line 664
  130. def OAI.MUB6.Certificate.PairSemantics.raw9085step1 line 666
  131. def OAI.MUB6.Certificate.PairSemantics.raw9085step2 line 668
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical9085 line 670
  133. def OAI.MUB6.Certificate.PairSemantics.raw9086 line 687
  134. def OAI.MUB6.Certificate.PairSemantics.raw9086step0 line 689
  135. def OAI.MUB6.Certificate.PairSemantics.raw9086step1 line 691
  136. theorem OAI.MUB6.Certificate.PairSemantics.canonical9086 line 693
  137. def OAI.MUB6.Certificate.PairSemantics.raw9087 line 706
  138. def OAI.MUB6.Certificate.PairSemantics.raw9087step0 line 708
  139. def OAI.MUB6.Certificate.PairSemantics.raw9087step1 line 710
  140. theorem OAI.MUB6.Certificate.PairSemantics.canonical9087 line 712