OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources40.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1280 line 30
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1280 line 31
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1280 line 32
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1280 line 33
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1280 line 35
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1281 line 224
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1281 line 225
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1281 line 226
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1281 line 227
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1281 line 229
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1282 line 418
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1282 line 419
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1282 line 420
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1282 line 421
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1282 line 423
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1283 line 612
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1283 line 613
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1283 line 614
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1283 line 615
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1283 line 617
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1284 line 668
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1284 line 669
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1284 line 670
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1284 line 671
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1284 line 673
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1285 line 724
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1285 line 725
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1285 line 726
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1285 line 727
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1285 line 729
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1286 line 918
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1286 line 919
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1286 line 920
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1286 line 921
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1286 line 923
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1287 line 1112
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1287 line 1113
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1287 line 1114
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1287 line 1115
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1287 line 1117
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1288 line 1306
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1288 line 1307
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1288 line 1308
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1288 line 1309
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1288 line 1311
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1289 line 1362
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1289 line 1363
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1289 line 1364
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1289 line 1365
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1289 line 1367
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1290 line 1418
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1290 line 1419
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1290 line 1420
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1290 line 1421
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1290 line 1423
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1291 line 1474
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1291 line 1475
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1291 line 1476
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1291 line 1477
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1291 line 1479
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1292 line 1668
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1292 line 1669
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1292 line 1670
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1292 line 1671
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1292 line 1673
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1293 line 1862
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1293 line 1863
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1293 line 1864
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1293 line 1865
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1293 line 1867
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1294 line 2056
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1294 line 2057
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1294 line 2058
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1294 line 2059
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1294 line 2061
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1295 line 2250
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1295 line 2251
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1295 line 2252
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1295 line 2253
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1295 line 2255
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1296 line 2306
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1296 line 2307
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1296 line 2308
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1296 line 2309
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1296 line 2311
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1297 line 2500
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1297 line 2501
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1297 line 2502
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1297 line 2503
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1297 line 2505
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1298 line 2694
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1298 line 2695
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1298 line 2696
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1298 line 2697
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1298 line 2699
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1299 line 2888
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1299 line 2889
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1299 line 2890
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1299 line 2891
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1299 line 2893
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1300 line 2944
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1300 line 2945
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1300 line 2946
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1300 line 2947
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1300 line 2949
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1301 line 3000
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1301 line 3001
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1301 line 3002
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1301 line 3003
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1301 line 3005
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1302 line 3056
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1302 line 3057
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1302 line 3058
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1302 line 3059
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1302 line 3061
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1303 line 3112
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1303 line 3113
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1303 line 3114
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1303 line 3115
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1303 line 3117
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1304 line 3306
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1304 line 3307
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1304 line 3308
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1304 line 3309
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1304 line 3311
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1305 line 3500
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1305 line 3501
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1305 line 3502
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1305 line 3503
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1305 line 3505
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1306 line 3694
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1306 line 3695
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1306 line 3696
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1306 line 3697
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1306 line 3699
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1307 line 3888
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1307 line 3889
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1307 line 3890
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1307 line 3891
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1307 line 3893
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1308 line 3944
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1308 line 3945
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1308 line 3946
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1308 line 3947
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1308 line 3949
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1309 line 4000
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1309 line 4001
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1309 line 4002
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1309 line 4003
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1309 line 4005
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1310 line 4056
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1310 line 4057
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1310 line 4058
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1310 line 4059
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1310 line 4061
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1311 line 4112
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1311 line 4113
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1311 line 4114
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1311 line 4115
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1311 line 4117