OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical240.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7680 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw7680step0 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw7680step1 line 15
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7680 line 17
  5. def OAI.MUB6.Certificate.PairSemantics.raw7681 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw7681step0 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7681 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw7682 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw7682step0 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7682 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw7683 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw7683step0 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7683 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw7684 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw7684step0 line 73
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7684 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw7685 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw7685step0 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw7685step1 line 88
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7685 line 90
  21. def OAI.MUB6.Certificate.PairSemantics.raw7686 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw7686step0 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw7686step1 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw7686step2 line 110
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7686 line 112
  26. def OAI.MUB6.Certificate.PairSemantics.raw7687 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw7687step0 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw7687step1 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw7687step2 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw7687step3 line 139
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7687 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw7688 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw7688step0 line 167
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7688 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw7689 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw7689step0 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw7689step1 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7689 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw7690 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw7690step0 line 200
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical7690 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw7691 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw7691step0 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw7691step1 line 215
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7691 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw7692 line 231
  47. def OAI.MUB6.Certificate.PairSemantics.raw7692step0 line 233
  48. def OAI.MUB6.Certificate.PairSemantics.raw7692step1 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw7692step2 line 237
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7692 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw7693 line 258
  52. def OAI.MUB6.Certificate.PairSemantics.raw7693step0 line 260
  53. def OAI.MUB6.Certificate.PairSemantics.raw7693step1 line 262
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7693 line 264
  55. def OAI.MUB6.Certificate.PairSemantics.raw7694 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw7694step0 line 280
  57. def OAI.MUB6.Certificate.PairSemantics.raw7694step1 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw7694step2 line 284
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7694 line 286
  60. def OAI.MUB6.Certificate.PairSemantics.raw7695 line 305
  61. def OAI.MUB6.Certificate.PairSemantics.raw7695step0 line 307
  62. def OAI.MUB6.Certificate.PairSemantics.raw7695step1 line 309
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical7695 line 311
  64. def OAI.MUB6.Certificate.PairSemantics.raw7696 line 325
  65. def OAI.MUB6.Certificate.PairSemantics.raw7696step0 line 327
  66. def OAI.MUB6.Certificate.PairSemantics.raw7696step1 line 329
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7696 line 331
  68. def OAI.MUB6.Certificate.PairSemantics.raw7697 line 345
  69. def OAI.MUB6.Certificate.PairSemantics.raw7697step0 line 347
  70. def OAI.MUB6.Certificate.PairSemantics.raw7697step1 line 349
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7697 line 351
  72. def OAI.MUB6.Certificate.PairSemantics.raw7698 line 365
  73. def OAI.MUB6.Certificate.PairSemantics.raw7698step0 line 367
  74. def OAI.MUB6.Certificate.PairSemantics.raw7698step1 line 369
  75. def OAI.MUB6.Certificate.PairSemantics.raw7698step2 line 371
  76. def OAI.MUB6.Certificate.PairSemantics.raw7698step3 line 373
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7698 line 375
  78. def OAI.MUB6.Certificate.PairSemantics.raw7699 line 399
  79. def OAI.MUB6.Certificate.PairSemantics.raw7699step0 line 401
  80. def OAI.MUB6.Certificate.PairSemantics.raw7699step1 line 403
  81. def OAI.MUB6.Certificate.PairSemantics.raw7699step2 line 405
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7699 line 407
  83. def OAI.MUB6.Certificate.PairSemantics.raw7700 line 426
  84. def OAI.MUB6.Certificate.PairSemantics.raw7700step0 line 428
  85. def OAI.MUB6.Certificate.PairSemantics.raw7700step1 line 430
  86. def OAI.MUB6.Certificate.PairSemantics.raw7700step2 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw7700step3 line 434
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7700 line 436
  89. def OAI.MUB6.Certificate.PairSemantics.raw7701 line 460
  90. def OAI.MUB6.Certificate.PairSemantics.raw7701step0 line 462
  91. def OAI.MUB6.Certificate.PairSemantics.raw7701step1 line 464
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7701 line 466
  93. def OAI.MUB6.Certificate.PairSemantics.raw7702 line 480
  94. def OAI.MUB6.Certificate.PairSemantics.raw7702step0 line 482
  95. def OAI.MUB6.Certificate.PairSemantics.raw7702step1 line 484
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7702 line 486
  97. def OAI.MUB6.Certificate.PairSemantics.raw7703 line 501
  98. def OAI.MUB6.Certificate.PairSemantics.raw7703step0 line 503
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7703 line 505
  100. def OAI.MUB6.Certificate.PairSemantics.raw7704 line 515
  101. def OAI.MUB6.Certificate.PairSemantics.raw7704step0 line 517
  102. def OAI.MUB6.Certificate.PairSemantics.raw7704step1 line 519
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7704 line 521
  104. def OAI.MUB6.Certificate.PairSemantics.raw7705 line 536
  105. def OAI.MUB6.Certificate.PairSemantics.raw7705step0 line 538
  106. def OAI.MUB6.Certificate.PairSemantics.raw7705step1 line 540
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7705 line 542
  108. def OAI.MUB6.Certificate.PairSemantics.raw7706 line 556
  109. def OAI.MUB6.Certificate.PairSemantics.raw7706step0 line 558
  110. def OAI.MUB6.Certificate.PairSemantics.raw7706step1 line 560
  111. def OAI.MUB6.Certificate.PairSemantics.raw7706step2 line 562
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7706 line 564
  113. def OAI.MUB6.Certificate.PairSemantics.raw7707 line 583
  114. def OAI.MUB6.Certificate.PairSemantics.raw7707step0 line 585
  115. def OAI.MUB6.Certificate.PairSemantics.raw7707step1 line 587
  116. def OAI.MUB6.Certificate.PairSemantics.raw7707step2 line 589
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical7707 line 591
  118. def OAI.MUB6.Certificate.PairSemantics.raw7708 line 610
  119. def OAI.MUB6.Certificate.PairSemantics.raw7708step0 line 612
  120. def OAI.MUB6.Certificate.PairSemantics.raw7708step1 line 614
  121. def OAI.MUB6.Certificate.PairSemantics.raw7708step2 line 616
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7708 line 618
  123. def OAI.MUB6.Certificate.PairSemantics.raw7709 line 638
  124. def OAI.MUB6.Certificate.PairSemantics.raw7709step0 line 640
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical7709 line 642
  126. def OAI.MUB6.Certificate.PairSemantics.raw7710 line 652
  127. def OAI.MUB6.Certificate.PairSemantics.raw7710step0 line 654
  128. def OAI.MUB6.Certificate.PairSemantics.raw7710step1 line 656
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical7710 line 658
  130. def OAI.MUB6.Certificate.PairSemantics.raw7711 line 672
  131. def OAI.MUB6.Certificate.PairSemantics.raw7711step0 line 674
  132. def OAI.MUB6.Certificate.PairSemantics.raw7711step1 line 676
  133. def OAI.MUB6.Certificate.PairSemantics.raw7711step2 line 678
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical7711 line 680