OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources85.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2720 line 14
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2720 line 15
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2720 line 16
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2720 line 17
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2720 line 19
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2721 line 70
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2721 line 71
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2721 line 72
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2721 line 73
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2721 line 75
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2722 line 126
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2722 line 127
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2722 line 128
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2722 line 129
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2722 line 131
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2723 line 182
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2723 line 183
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2723 line 184
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2723 line 185
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2723 line 187
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2724 line 238
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2724 line 239
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2724 line 240
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2724 line 241
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2724 line 243
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2725 line 294
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2725 line 295
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2725 line 296
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2725 line 297
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2725 line 299
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2726 line 350
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2726 line 351
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2726 line 352
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2726 line 353
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2726 line 355
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2727 line 406
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2727 line 407
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2727 line 408
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2727 line 409
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2727 line 411
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2728 line 462
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2728 line 463
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2728 line 464
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2728 line 465
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2728 line 467
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2729 line 518
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2729 line 519
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2729 line 520
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2729 line 521
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2729 line 523
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2730 line 574
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2730 line 575
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2730 line 576
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2730 line 577
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2730 line 579
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2731 line 630
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2731 line 631
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2731 line 632
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2731 line 633
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2731 line 635
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2732 line 686
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2732 line 687
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2732 line 688
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2732 line 689
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2732 line 691
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2733 line 742
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2733 line 743
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2733 line 744
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2733 line 745
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2733 line 747
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2734 line 798
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2734 line 799
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2734 line 800
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2734 line 801
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2734 line 803
  76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2735 line 854
  77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2735 line 855
  78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2735 line 856
  79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2735 line 857
  80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2735 line 859
  81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2736 line 910
  82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2736 line 911
  83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2736 line 912
  84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2736 line 913
  85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2736 line 915
  86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2737 line 966
  87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2737 line 967
  88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2737 line 968
  89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2737 line 969
  90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2737 line 971
  91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2738 line 1022
  92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2738 line 1023
  93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2738 line 1024
  94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2738 line 1025
  95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2738 line 1027
  96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2739 line 1078
  97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2739 line 1079
  98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2739 line 1080
  99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2739 line 1081
  100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2739 line 1083
  101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2740 line 1134
  102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2740 line 1135
  103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2740 line 1136
  104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2740 line 1137
  105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2740 line 1139
  106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2741 line 1190
  107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2741 line 1191
  108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2741 line 1192
  109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2741 line 1193
  110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2741 line 1195
  111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2742 line 1246
  112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2742 line 1247
  113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2742 line 1248
  114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2742 line 1249
  115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2742 line 1251
  116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2743 line 1302
  117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2743 line 1303
  118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2743 line 1304
  119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2743 line 1305
  120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2743 line 1307
  121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2744 line 1358
  122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2744 line 1359
  123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2744 line 1360
  124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2744 line 1361
  125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2744 line 1363
  126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2745 line 1414
  127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2745 line 1415
  128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2745 line 1416
  129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2745 line 1417
  130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2745 line 1419
  131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2746 line 1470
  132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2746 line 1471
  133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2746 line 1472
  134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2746 line 1473
  135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2746 line 1475
  136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2747 line 1526
  137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2747 line 1527
  138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2747 line 1528
  139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2747 line 1529
  140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2747 line 1531
  141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2748 line 1582
  142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2748 line 1583
  143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2748 line 1584
  144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2748 line 1585
  145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2748 line 1587
  146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2749 line 1638
  147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2749 line 1639
  148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2749 line 1640
  149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2749 line 1641
  150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2749 line 1643
  151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2750 line 1694
  152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2750 line 1695
  153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2750 line 1696
  154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2750 line 1697
  155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2750 line 1699
  156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2751 line 1750
  157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2751 line 1751
  158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2751 line 1752
  159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2751 line 1753
  160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2751 line 1755