OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources41.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1312 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1312 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1312 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1312 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1312 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1313 line 77
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1313 line 78
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1313 line 79
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1313 line 80
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1313 line 82
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1314 line 133
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1314 line 134
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1314 line 135
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1314 line 136
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1314 line 138
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1315 line 189
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1315 line 190
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1315 line 191
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1315 line 192
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1315 line 194
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1316 line 245
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1316 line 246
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1316 line 247
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1316 line 248
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1316 line 250
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1317 line 301
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1317 line 302
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1317 line 303
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1317 line 304
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1317 line 306
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1318 line 357
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1318 line 358
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1318 line 359
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1318 line 360
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1318 line 362
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1319 line 413
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1319 line 414
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1319 line 415
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1319 line 416
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1319 line 418
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1320 line 469
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1320 line 470
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1320 line 471
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1320 line 472
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1320 line 474
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1321 line 525
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1321 line 526
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1321 line 527
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1321 line 528
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1321 line 530
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1322 line 581
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1322 line 582
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1322 line 583
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1322 line 584
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1322 line 586
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1323 line 637
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1323 line 638
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1323 line 639
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1323 line 640
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1323 line 642
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1324 line 693
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1324 line 694
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1324 line 695
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1324 line 696
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1324 line 698
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1325 line 749
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1325 line 750
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1325 line 751
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1325 line 752
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1325 line 754
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1326 line 805
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1326 line 806
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1326 line 807
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1326 line 808
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1326 line 810
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1327 line 861
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1327 line 862
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1327 line 863
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1327 line 864
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1327 line 866
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1328 line 917
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1328 line 918
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1328 line 919
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1328 line 920
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1328 line 922
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1329 line 973
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1329 line 974
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1329 line 975
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1329 line 976
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1329 line 978
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1330 line 1029
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1330 line 1030
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1330 line 1031
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1330 line 1032
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1330 line 1034
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1331 line 1085
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1331 line 1086
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1331 line 1087
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1331 line 1088
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1331 line 1090
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1332 line 1141
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1332 line 1142
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1332 line 1143
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1332 line 1144
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1332 line 1146
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1333 line 1197
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1333 line 1198
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1333 line 1199
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1333 line 1200
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1333 line 1202
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1334 line 1253
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1334 line 1254
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1334 line 1255
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1334 line 1256
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1334 line 1258
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1335 line 1309
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1335 line 1310
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1335 line 1311
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1335 line 1312
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1335 line 1314
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1336 line 1503
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1336 line 1504
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1336 line 1505
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1336 line 1506
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1336 line 1508
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1337 line 1697
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1337 line 1698
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1337 line 1699
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1337 line 1700
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1337 line 1702
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1338 line 1891
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1338 line 1892
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1338 line 1893
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1338 line 1894
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1338 line 1896
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1339 line 1947
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1339 line 1948
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1339 line 1949
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1339 line 1950
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1339 line 1952
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1340 line 2003
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1340 line 2004
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1340 line 2005
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1340 line 2006
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1340 line 2008
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1341 line 2059
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1341 line 2060
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1341 line 2061
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1341 line 2062
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1341 line 2064
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1342 line 2115
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1342 line 2116
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1342 line 2117
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1342 line 2118
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1342 line 2120
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1343 line 2309
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1343 line 2310
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1343 line 2311
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1343 line 2312
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1343 line 2314