OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources50.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1600 line 26
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1600 line 27
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1600 line 28
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1600 line 29
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1600 line 31
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1601 line 82
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1601 line 83
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1601 line 84
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1601 line 85
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1601 line 87
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1602 line 138
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1602 line 139
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1602 line 140
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1602 line 141
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1602 line 143
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1603 line 194
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1603 line 195
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1603 line 196
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1603 line 197
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1603 line 199
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1604 line 250
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1604 line 251
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1604 line 252
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1604 line 253
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1604 line 255
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1605 line 306
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1605 line 307
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1605 line 308
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1605 line 309
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1605 line 311
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1606 line 362
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1606 line 363
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1606 line 364
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1606 line 365
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1606 line 367
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1607 line 418
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1607 line 419
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1607 line 420
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1607 line 421
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1607 line 423
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1608 line 474
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1608 line 475
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1608 line 476
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1608 line 477
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1608 line 479
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1609 line 530
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1609 line 531
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1609 line 532
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1609 line 533
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1609 line 535
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1610 line 586
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1610 line 587
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1610 line 588
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1610 line 589
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1610 line 591
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1611 line 642
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1611 line 643
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1611 line 644
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1611 line 645
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1611 line 647
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1612 line 698
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1612 line 699
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1612 line 700
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1612 line 701
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1612 line 703
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1613 line 754
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1613 line 755
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1613 line 756
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1613 line 757
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1613 line 759
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1614 line 810
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1614 line 811
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1614 line 812
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1614 line 813
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1614 line 815
  76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1615 line 866
  77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1615 line 867
  78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1615 line 868
  79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1615 line 869
  80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1615 line 871
  81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1616 line 922
  82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1616 line 923
  83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1616 line 924
  84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1616 line 925
  85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1616 line 927
  86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1617 line 978
  87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1617 line 979
  88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1617 line 980
  89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1617 line 981
  90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1617 line 983
  91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1618 line 1034
  92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1618 line 1035
  93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1618 line 1036
  94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1618 line 1037
  95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1618 line 1039
  96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1619 line 1090
  97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1619 line 1091
  98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1619 line 1092
  99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1619 line 1093
  100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1619 line 1095
  101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1620 line 1146
  102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1620 line 1147
  103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1620 line 1148
  104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1620 line 1149
  105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1620 line 1151
  106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1621 line 1202
  107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1621 line 1203
  108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1621 line 1204
  109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1621 line 1205
  110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1621 line 1207
  111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1622 line 1258
  112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1622 line 1259
  113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1622 line 1260
  114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1622 line 1261
  115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1622 line 1263
  116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1623 line 1314
  117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1623 line 1315
  118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1623 line 1316
  119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1623 line 1317
  120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1623 line 1319
  121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1624 line 1370
  122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1624 line 1371
  123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1624 line 1372
  124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1624 line 1373
  125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1624 line 1375
  126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1625 line 1426
  127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1625 line 1427
  128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1625 line 1428
  129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1625 line 1429
  130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1625 line 1431
  131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1626 line 1482
  132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1626 line 1483
  133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1626 line 1484
  134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1626 line 1485
  135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1626 line 1487
  136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1627 line 1538
  137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1627 line 1539
  138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1627 line 1540
  139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1627 line 1541
  140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1627 line 1543
  141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1628 line 1594
  142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1628 line 1595
  143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1628 line 1596
  144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1628 line 1597
  145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1628 line 1599
  146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1629 line 1650
  147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1629 line 1651
  148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1629 line 1652
  149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1629 line 1653
  150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1629 line 1655
  151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1630 line 1706
  152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1630 line 1707
  153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1630 line 1708
  154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1630 line 1709
  155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1630 line 1711
  156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1631 line 1762
  157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1631 line 1763
  158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1631 line 1764
  159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1631 line 1765
  160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1631 line 1767