OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical303.lean

GitHub source file

143 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9696 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw9696step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw9696step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9696 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw9697 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw9697step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw9697step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9697 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw9698 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw9698step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw9698step1 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw9698step2 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9698 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw9699 line 86
  15. def OAI.MUB6.Certificate.PairSemantics.raw9699step0 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw9699step1 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw9699step2 line 92
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9699 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw9700 line 112
  20. def OAI.MUB6.Certificate.PairSemantics.raw9700step0 line 114
  21. def OAI.MUB6.Certificate.PairSemantics.raw9700step1 line 116
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9700 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw9701 line 132
  24. def OAI.MUB6.Certificate.PairSemantics.raw9701step0 line 134
  25. def OAI.MUB6.Certificate.PairSemantics.raw9701step1 line 136
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9701 line 138
  27. def OAI.MUB6.Certificate.PairSemantics.raw9702 line 152
  28. def OAI.MUB6.Certificate.PairSemantics.raw9702step0 line 154
  29. def OAI.MUB6.Certificate.PairSemantics.raw9702step1 line 156
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9702 line 158
  31. def OAI.MUB6.Certificate.PairSemantics.raw9703 line 172
  32. def OAI.MUB6.Certificate.PairSemantics.raw9703step0 line 174
  33. def OAI.MUB6.Certificate.PairSemantics.raw9703step1 line 176
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9703 line 178
  35. def OAI.MUB6.Certificate.PairSemantics.raw9704 line 192
  36. def OAI.MUB6.Certificate.PairSemantics.raw9704step0 line 194
  37. def OAI.MUB6.Certificate.PairSemantics.raw9704step1 line 196
  38. def OAI.MUB6.Certificate.PairSemantics.raw9704step2 line 198
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9704 line 200
  40. def OAI.MUB6.Certificate.PairSemantics.raw9705 line 218
  41. def OAI.MUB6.Certificate.PairSemantics.raw9705step0 line 220
  42. def OAI.MUB6.Certificate.PairSemantics.raw9705step1 line 222
  43. def OAI.MUB6.Certificate.PairSemantics.raw9705step2 line 224
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9705 line 226
  45. def OAI.MUB6.Certificate.PairSemantics.raw9706 line 244
  46. def OAI.MUB6.Certificate.PairSemantics.raw9706step0 line 246
  47. def OAI.MUB6.Certificate.PairSemantics.raw9706step1 line 248
  48. def OAI.MUB6.Certificate.PairSemantics.raw9706step2 line 250
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9706 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw9707 line 270
  51. def OAI.MUB6.Certificate.PairSemantics.raw9707step0 line 272
  52. def OAI.MUB6.Certificate.PairSemantics.raw9707step1 line 274
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9707 line 276
  54. def OAI.MUB6.Certificate.PairSemantics.raw9708 line 290
  55. def OAI.MUB6.Certificate.PairSemantics.raw9708step0 line 292
  56. def OAI.MUB6.Certificate.PairSemantics.raw9708step1 line 294
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9708 line 296
  58. def OAI.MUB6.Certificate.PairSemantics.raw9709 line 310
  59. def OAI.MUB6.Certificate.PairSemantics.raw9709step0 line 312
  60. def OAI.MUB6.Certificate.PairSemantics.raw9709step1 line 314
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9709 line 316
  62. def OAI.MUB6.Certificate.PairSemantics.raw9710 line 330
  63. def OAI.MUB6.Certificate.PairSemantics.raw9710step0 line 332
  64. def OAI.MUB6.Certificate.PairSemantics.raw9710step1 line 334
  65. def OAI.MUB6.Certificate.PairSemantics.raw9710step2 line 336
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9710 line 338
  67. def OAI.MUB6.Certificate.PairSemantics.raw9711 line 356
  68. def OAI.MUB6.Certificate.PairSemantics.raw9711step0 line 358
  69. def OAI.MUB6.Certificate.PairSemantics.raw9711step1 line 360
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9711 line 362
  71. def OAI.MUB6.Certificate.PairSemantics.raw9712 line 376
  72. def OAI.MUB6.Certificate.PairSemantics.raw9712step0 line 378
  73. def OAI.MUB6.Certificate.PairSemantics.raw9712step1 line 380
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9712 line 382
  75. def OAI.MUB6.Certificate.PairSemantics.raw9713 line 396
  76. def OAI.MUB6.Certificate.PairSemantics.raw9713step0 line 398
  77. def OAI.MUB6.Certificate.PairSemantics.raw9713step1 line 400
  78. def OAI.MUB6.Certificate.PairSemantics.raw9713step2 line 402
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9713 line 404
  80. def OAI.MUB6.Certificate.PairSemantics.raw9714 line 422
  81. def OAI.MUB6.Certificate.PairSemantics.raw9714step0 line 424
  82. def OAI.MUB6.Certificate.PairSemantics.raw9714step1 line 426
  83. def OAI.MUB6.Certificate.PairSemantics.raw9714step2 line 428
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9714 line 430
  85. def OAI.MUB6.Certificate.PairSemantics.raw9715 line 448
  86. def OAI.MUB6.Certificate.PairSemantics.raw9715step0 line 450
  87. def OAI.MUB6.Certificate.PairSemantics.raw9715step1 line 452
  88. def OAI.MUB6.Certificate.PairSemantics.raw9715step2 line 454
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9715 line 456
  90. def OAI.MUB6.Certificate.PairSemantics.raw9716 line 474
  91. def OAI.MUB6.Certificate.PairSemantics.raw9716step0 line 476
  92. def OAI.MUB6.Certificate.PairSemantics.raw9716step1 line 478
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9716 line 480
  94. def OAI.MUB6.Certificate.PairSemantics.raw9717 line 494
  95. def OAI.MUB6.Certificate.PairSemantics.raw9717step0 line 496
  96. def OAI.MUB6.Certificate.PairSemantics.raw9717step1 line 498
  97. def OAI.MUB6.Certificate.PairSemantics.raw9717step2 line 500
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9717 line 502
  99. def OAI.MUB6.Certificate.PairSemantics.raw9718 line 520
  100. def OAI.MUB6.Certificate.PairSemantics.raw9718step0 line 522
  101. def OAI.MUB6.Certificate.PairSemantics.raw9718step1 line 524
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9718 line 526
  103. def OAI.MUB6.Certificate.PairSemantics.raw9719 line 540
  104. def OAI.MUB6.Certificate.PairSemantics.raw9719step0 line 542
  105. def OAI.MUB6.Certificate.PairSemantics.raw9719step1 line 544
  106. def OAI.MUB6.Certificate.PairSemantics.raw9719step2 line 546
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9719 line 548
  108. def OAI.MUB6.Certificate.PairSemantics.raw9720 line 566
  109. def OAI.MUB6.Certificate.PairSemantics.raw9720step0 line 568
  110. def OAI.MUB6.Certificate.PairSemantics.raw9720step1 line 570
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical9720 line 572
  112. def OAI.MUB6.Certificate.PairSemantics.raw9721 line 586
  113. def OAI.MUB6.Certificate.PairSemantics.raw9721step0 line 588
  114. def OAI.MUB6.Certificate.PairSemantics.raw9721step1 line 590
  115. def OAI.MUB6.Certificate.PairSemantics.raw9721step2 line 592
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical9721 line 594
  117. def OAI.MUB6.Certificate.PairSemantics.raw9722 line 612
  118. def OAI.MUB6.Certificate.PairSemantics.raw9722step0 line 614
  119. def OAI.MUB6.Certificate.PairSemantics.raw9722step1 line 616
  120. def OAI.MUB6.Certificate.PairSemantics.raw9722step2 line 618
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical9722 line 620
  122. def OAI.MUB6.Certificate.PairSemantics.raw9723 line 638
  123. def OAI.MUB6.Certificate.PairSemantics.raw9723step0 line 640
  124. def OAI.MUB6.Certificate.PairSemantics.raw9723step1 line 642
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical9723 line 644
  126. def OAI.MUB6.Certificate.PairSemantics.raw9724 line 658
  127. def OAI.MUB6.Certificate.PairSemantics.raw9724step0 line 660
  128. def OAI.MUB6.Certificate.PairSemantics.raw9724step1 line 662
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical9724 line 664
  130. def OAI.MUB6.Certificate.PairSemantics.raw9725 line 678
  131. def OAI.MUB6.Certificate.PairSemantics.raw9725step0 line 680
  132. def OAI.MUB6.Certificate.PairSemantics.raw9725step1 line 682
  133. def OAI.MUB6.Certificate.PairSemantics.raw9725step2 line 684
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical9725 line 686
  135. def OAI.MUB6.Certificate.PairSemantics.raw9726 line 704
  136. def OAI.MUB6.Certificate.PairSemantics.raw9726step0 line 706
  137. def OAI.MUB6.Certificate.PairSemantics.raw9726step1 line 708
  138. def OAI.MUB6.Certificate.PairSemantics.raw9726step2 line 710
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical9726 line 712
  140. def OAI.MUB6.Certificate.PairSemantics.raw9727 line 730
  141. def OAI.MUB6.Certificate.PairSemantics.raw9727step0 line 732
  142. def OAI.MUB6.Certificate.PairSemantics.raw9727step1 line 734
  143. theorem OAI.MUB6.Certificate.PairSemantics.canonical9727 line 736