OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources84.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2688 line 13
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2688 line 14
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2688 line 15
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2688 line 16
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2688 line 18
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2689 line 69
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2689 line 70
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2689 line 71
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2689 line 72
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2689 line 74
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2690 line 125
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2690 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2690 line 127
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2690 line 128
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2690 line 130
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2691 line 181
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2691 line 182
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2691 line 183
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2691 line 184
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2691 line 186
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2692 line 237
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2692 line 238
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2692 line 239
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2692 line 240
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2692 line 242
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2693 line 293
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2693 line 294
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2693 line 295
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2693 line 296
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2693 line 298
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2694 line 349
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2694 line 350
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2694 line 351
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2694 line 352
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2694 line 354
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2695 line 405
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2695 line 406
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2695 line 407
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2695 line 408
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2695 line 410
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2696 line 461
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2696 line 462
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2696 line 463
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2696 line 464
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2696 line 466
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2697 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2697 line 518
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2697 line 519
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2697 line 520
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2697 line 522
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2698 line 573
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2698 line 574
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2698 line 575
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2698 line 576
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2698 line 578
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2699 line 629
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2699 line 630
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2699 line 631
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2699 line 632
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2699 line 634
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2700 line 685
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2700 line 686
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2700 line 687
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2700 line 688
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2700 line 690
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2701 line 741
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2701 line 742
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2701 line 743
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2701 line 744
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2701 line 746
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2702 line 797
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2702 line 798
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2702 line 799
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2702 line 800
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2702 line 802
  76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2703 line 853
  77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2703 line 854
  78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2703 line 855
  79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2703 line 856
  80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2703 line 858
  81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2704 line 909
  82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2704 line 910
  83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2704 line 911
  84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2704 line 912
  85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2704 line 914
  86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2705 line 965
  87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2705 line 966
  88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2705 line 967
  89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2705 line 968
  90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2705 line 970
  91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2706 line 1021
  92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2706 line 1022
  93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2706 line 1023
  94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2706 line 1024
  95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2706 line 1026
  96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2707 line 1077
  97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2707 line 1078
  98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2707 line 1079
  99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2707 line 1080
  100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2707 line 1082
  101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2708 line 1133
  102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2708 line 1134
  103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2708 line 1135
  104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2708 line 1136
  105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2708 line 1138
  106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2709 line 1189
  107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2709 line 1190
  108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2709 line 1191
  109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2709 line 1192
  110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2709 line 1194
  111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2710 line 1245
  112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2710 line 1246
  113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2710 line 1247
  114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2710 line 1248
  115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2710 line 1250
  116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2711 line 1301
  117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2711 line 1302
  118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2711 line 1303
  119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2711 line 1304
  120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2711 line 1306
  121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2712 line 1357
  122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2712 line 1358
  123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2712 line 1359
  124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2712 line 1360
  125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2712 line 1362
  126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2713 line 1413
  127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2713 line 1414
  128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2713 line 1415
  129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2713 line 1416
  130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2713 line 1418
  131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2714 line 1469
  132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2714 line 1470
  133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2714 line 1471
  134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2714 line 1472
  135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2714 line 1474
  136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2715 line 1525
  137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2715 line 1526
  138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2715 line 1527
  139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2715 line 1528
  140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2715 line 1530
  141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2716 line 1581
  142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2716 line 1582
  143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2716 line 1583
  144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2716 line 1584
  145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2716 line 1586
  146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2717 line 1637
  147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2717 line 1638
  148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2717 line 1639
  149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2717 line 1640
  150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2717 line 1642
  151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2718 line 1693
  152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2718 line 1694
  153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2718 line 1695
  154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2718 line 1696
  155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2718 line 1698
  156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2719 line 1749
  157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2719 line 1750
  158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2719 line 1751
  159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2719 line 1752
  160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2719 line 1754