OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical82.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2624 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw2624step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw2624step1 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw2624step2 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2624 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw2625 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw2625step0 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw2625step1 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2625 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw2626 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw2626step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw2626step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2626 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw2627 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw2627step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw2627step1 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw2627step2 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2627 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw2628 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw2628step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw2628step1 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw2628step2 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2628 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw2629 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw2629step0 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw2629step1 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2629 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw2630 line 151
  29. def OAI.MUB6.Certificate.PairSemantics.raw2630step0 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw2630step1 line 155
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2630 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw2631 line 170
  33. def OAI.MUB6.Certificate.PairSemantics.raw2631step0 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw2631step1 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw2631step2 line 176
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2631 line 178
  37. def OAI.MUB6.Certificate.PairSemantics.raw2632 line 195
  38. def OAI.MUB6.Certificate.PairSemantics.raw2632step0 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw2632step1 line 199
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2632 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw2633 line 214
  42. def OAI.MUB6.Certificate.PairSemantics.raw2633step0 line 216
  43. def OAI.MUB6.Certificate.PairSemantics.raw2633step1 line 218
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2633 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw2634 line 233
  46. def OAI.MUB6.Certificate.PairSemantics.raw2634step0 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw2634step1 line 237
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2634 line 239
  49. def OAI.MUB6.Certificate.PairSemantics.raw2635 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw2635step0 line 254
  51. def OAI.MUB6.Certificate.PairSemantics.raw2635step1 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw2635step2 line 258
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2635 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw2636 line 277
  55. def OAI.MUB6.Certificate.PairSemantics.raw2636step0 line 279
  56. def OAI.MUB6.Certificate.PairSemantics.raw2636step1 line 281
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2636 line 283
  58. def OAI.MUB6.Certificate.PairSemantics.raw2637 line 296
  59. def OAI.MUB6.Certificate.PairSemantics.raw2637step0 line 298
  60. def OAI.MUB6.Certificate.PairSemantics.raw2637step1 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw2637step2 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2637 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw2638 line 321
  64. def OAI.MUB6.Certificate.PairSemantics.raw2638step0 line 323
  65. def OAI.MUB6.Certificate.PairSemantics.raw2638step1 line 325
  66. def OAI.MUB6.Certificate.PairSemantics.raw2638step2 line 327
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2638 line 329
  68. def OAI.MUB6.Certificate.PairSemantics.raw2639 line 346
  69. def OAI.MUB6.Certificate.PairSemantics.raw2639step0 line 348
  70. def OAI.MUB6.Certificate.PairSemantics.raw2639step1 line 350
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2639 line 352
  72. def OAI.MUB6.Certificate.PairSemantics.raw2640 line 365
  73. def OAI.MUB6.Certificate.PairSemantics.raw2640step0 line 367
  74. def OAI.MUB6.Certificate.PairSemantics.raw2640step1 line 369
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2640 line 371
  76. def OAI.MUB6.Certificate.PairSemantics.raw2641 line 384
  77. def OAI.MUB6.Certificate.PairSemantics.raw2641step0 line 386
  78. def OAI.MUB6.Certificate.PairSemantics.raw2641step1 line 388
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2641 line 390
  80. def OAI.MUB6.Certificate.PairSemantics.raw2642 line 403
  81. def OAI.MUB6.Certificate.PairSemantics.raw2642step0 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw2642step1 line 407
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2642 line 409
  84. def OAI.MUB6.Certificate.PairSemantics.raw2643 line 422
  85. def OAI.MUB6.Certificate.PairSemantics.raw2643step0 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw2643step1 line 426
  87. def OAI.MUB6.Certificate.PairSemantics.raw2643step2 line 428
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2643 line 430
  89. def OAI.MUB6.Certificate.PairSemantics.raw2644 line 447
  90. def OAI.MUB6.Certificate.PairSemantics.raw2644step0 line 449
  91. def OAI.MUB6.Certificate.PairSemantics.raw2644step1 line 451
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2644 line 453
  93. def OAI.MUB6.Certificate.PairSemantics.raw2645 line 466
  94. def OAI.MUB6.Certificate.PairSemantics.raw2645step0 line 468
  95. def OAI.MUB6.Certificate.PairSemantics.raw2645step1 line 470
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2645 line 472
  97. def OAI.MUB6.Certificate.PairSemantics.raw2646 line 485
  98. def OAI.MUB6.Certificate.PairSemantics.raw2646step0 line 487
  99. def OAI.MUB6.Certificate.PairSemantics.raw2646step1 line 489
  100. def OAI.MUB6.Certificate.PairSemantics.raw2646step2 line 491
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2646 line 493
  102. def OAI.MUB6.Certificate.PairSemantics.raw2647 line 510
  103. def OAI.MUB6.Certificate.PairSemantics.raw2647step0 line 512
  104. def OAI.MUB6.Certificate.PairSemantics.raw2647step1 line 514
  105. def OAI.MUB6.Certificate.PairSemantics.raw2647step2 line 516
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical2647 line 518
  107. def OAI.MUB6.Certificate.PairSemantics.raw2648 line 535
  108. def OAI.MUB6.Certificate.PairSemantics.raw2648step0 line 537
  109. def OAI.MUB6.Certificate.PairSemantics.raw2648step1 line 539
  110. def OAI.MUB6.Certificate.PairSemantics.raw2648step2 line 541
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical2648 line 543
  112. def OAI.MUB6.Certificate.PairSemantics.raw2649 line 560
  113. def OAI.MUB6.Certificate.PairSemantics.raw2649step0 line 562
  114. def OAI.MUB6.Certificate.PairSemantics.raw2649step1 line 564
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical2649 line 566
  116. def OAI.MUB6.Certificate.PairSemantics.raw2650 line 579
  117. def OAI.MUB6.Certificate.PairSemantics.raw2650step0 line 581
  118. def OAI.MUB6.Certificate.PairSemantics.raw2650step1 line 583
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical2650 line 585
  120. def OAI.MUB6.Certificate.PairSemantics.raw2651 line 598
  121. def OAI.MUB6.Certificate.PairSemantics.raw2651step0 line 600
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical2651 line 602
  123. def OAI.MUB6.Certificate.PairSemantics.raw2652 line 611
  124. def OAI.MUB6.Certificate.PairSemantics.raw2652step0 line 613
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical2652 line 615
  126. def OAI.MUB6.Certificate.PairSemantics.raw2653 line 624
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical2653 line 626
  128. def OAI.MUB6.Certificate.PairSemantics.raw2654 line 630
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical2654 line 632
  130. def OAI.MUB6.Certificate.PairSemantics.raw2655 line 636
  131. def OAI.MUB6.Certificate.PairSemantics.raw2655step0 line 638
  132. def OAI.MUB6.Certificate.PairSemantics.raw2655step1 line 640
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical2655 line 642