OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources83.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2656 line 13
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2656 line 14
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2656 line 15
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2656 line 16
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2656 line 18
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2657 line 69
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2657 line 70
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2657 line 71
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2657 line 72
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2657 line 74
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2658 line 125
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2658 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2658 line 127
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2658 line 128
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2658 line 130
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2659 line 181
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2659 line 182
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2659 line 183
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2659 line 184
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2659 line 186
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2660 line 237
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2660 line 238
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2660 line 239
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2660 line 240
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2660 line 242
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2661 line 293
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2661 line 294
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2661 line 295
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2661 line 296
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2661 line 298
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2662 line 349
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2662 line 350
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2662 line 351
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2662 line 352
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2662 line 354
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2663 line 405
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2663 line 406
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2663 line 407
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2663 line 408
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2663 line 410
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2664 line 461
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2664 line 462
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2664 line 463
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2664 line 464
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2664 line 466
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2665 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2665 line 518
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2665 line 519
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2665 line 520
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2665 line 522
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2666 line 573
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2666 line 574
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2666 line 575
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2666 line 576
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2666 line 578
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2667 line 629
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2667 line 630
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2667 line 631
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2667 line 632
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2667 line 634
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2668 line 685
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2668 line 686
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2668 line 687
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2668 line 688
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2668 line 690
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2669 line 741
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2669 line 742
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2669 line 743
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2669 line 744
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2669 line 746
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2670 line 797
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2670 line 798
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2670 line 799
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2670 line 800
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2670 line 802
  76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2671 line 853
  77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2671 line 854
  78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2671 line 855
  79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2671 line 856
  80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2671 line 858
  81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2672 line 909
  82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2672 line 910
  83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2672 line 911
  84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2672 line 912
  85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2672 line 914
  86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2673 line 965
  87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2673 line 966
  88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2673 line 967
  89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2673 line 968
  90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2673 line 970
  91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2674 line 1021
  92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2674 line 1022
  93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2674 line 1023
  94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2674 line 1024
  95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2674 line 1026
  96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2675 line 1077
  97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2675 line 1078
  98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2675 line 1079
  99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2675 line 1080
  100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2675 line 1082
  101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2676 line 1133
  102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2676 line 1134
  103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2676 line 1135
  104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2676 line 1136
  105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2676 line 1138
  106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2677 line 1189
  107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2677 line 1190
  108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2677 line 1191
  109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2677 line 1192
  110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2677 line 1194
  111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2678 line 1245
  112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2678 line 1246
  113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2678 line 1247
  114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2678 line 1248
  115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2678 line 1250
  116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2679 line 1301
  117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2679 line 1302
  118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2679 line 1303
  119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2679 line 1304
  120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2679 line 1306
  121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2680 line 1357
  122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2680 line 1358
  123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2680 line 1359
  124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2680 line 1360
  125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2680 line 1362
  126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2681 line 1413
  127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2681 line 1414
  128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2681 line 1415
  129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2681 line 1416
  130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2681 line 1418
  131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2682 line 1469
  132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2682 line 1470
  133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2682 line 1471
  134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2682 line 1472
  135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2682 line 1474
  136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2683 line 1525
  137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2683 line 1526
  138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2683 line 1527
  139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2683 line 1528
  140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2683 line 1530
  141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2684 line 1581
  142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2684 line 1582
  143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2684 line 1583
  144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2684 line 1584
  145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2684 line 1586
  146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2685 line 1637
  147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2685 line 1638
  148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2685 line 1639
  149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2685 line 1640
  150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2685 line 1642
  151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2686 line 1693
  152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2686 line 1694
  153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2686 line 1695
  154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2686 line 1696
  155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2686 line 1698
  156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2687 line 1749
  157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2687 line 1750
  158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2687 line 1751
  159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2687 line 1752
  160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2687 line 1754