OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources49.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1568 line 28
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1568 line 29
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1568 line 30
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1568 line 31
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1568 line 33
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1569 line 84
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1569 line 85
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1569 line 86
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1569 line 87
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1569 line 89
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1570 line 278
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1570 line 279
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1570 line 280
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1570 line 281
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1570 line 283
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1571 line 472
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1571 line 473
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1571 line 474
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1571 line 475
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1571 line 477
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1572 line 528
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1572 line 529
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1572 line 530
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1572 line 531
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1572 line 533
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1573 line 584
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1573 line 585
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1573 line 586
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1573 line 587
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1573 line 589
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1574 line 640
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1574 line 641
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1574 line 642
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1574 line 643
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1574 line 645
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1575 line 834
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1575 line 835
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1575 line 836
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1575 line 837
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1575 line 839
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1576 line 1028
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1576 line 1029
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1576 line 1030
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1576 line 1031
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1576 line 1033
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1577 line 1084
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1577 line 1085
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1577 line 1086
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1577 line 1087
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1577 line 1089
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1578 line 1140
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1578 line 1141
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1578 line 1142
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1578 line 1143
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1578 line 1145
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1579 line 1196
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1579 line 1197
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1579 line 1198
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1579 line 1199
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1579 line 1201
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1580 line 1252
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1580 line 1253
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1580 line 1254
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1580 line 1255
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1580 line 1257
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1581 line 1308
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1581 line 1309
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1581 line 1310
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1581 line 1311
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1581 line 1313
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1582 line 1364
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1582 line 1365
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1582 line 1366
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1582 line 1367
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1582 line 1369
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1583 line 1420
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1583 line 1421
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1583 line 1422
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1583 line 1423
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1583 line 1425
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1584 line 1476
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1584 line 1477
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1584 line 1478
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1584 line 1479
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1584 line 1481
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1585 line 1532
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1585 line 1533
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1585 line 1534
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1585 line 1535
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1585 line 1537
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1586 line 1588
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1586 line 1589
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1586 line 1590
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1586 line 1591
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1586 line 1593
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1587 line 1644
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1587 line 1645
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1587 line 1646
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1587 line 1647
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1587 line 1649
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1588 line 1700
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1588 line 1701
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1588 line 1702
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1588 line 1703
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1588 line 1705
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1589 line 1756
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1589 line 1757
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1589 line 1758
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1589 line 1759
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1589 line 1761
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1590 line 1812
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1590 line 1813
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1590 line 1814
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1590 line 1815
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1590 line 1817
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1591 line 1868
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1591 line 1869
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1591 line 1870
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1591 line 1871
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1591 line 1873
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1592 line 1924
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1592 line 1925
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1592 line 1926
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1592 line 1927
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1592 line 1929
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1593 line 1980
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1593 line 1981
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1593 line 1982
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1593 line 1983
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1593 line 1985
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1594 line 2036
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1594 line 2037
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1594 line 2038
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1594 line 2039
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1594 line 2041
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1595 line 2092
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1595 line 2093
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1595 line 2094
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1595 line 2095
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1595 line 2097
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1596 line 2148
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1596 line 2149
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1596 line 2150
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1596 line 2151
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1596 line 2153
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1597 line 2204
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1597 line 2205
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1597 line 2206
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1597 line 2207
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1597 line 2209
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1598 line 2260
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1598 line 2261
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1598 line 2262
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1598 line 2263
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1598 line 2265
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1599 line 2316
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1599 line 2317
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1599 line 2318
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1599 line 2319
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1599 line 2321