OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources37.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1184 line 24
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1184 line 25
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1184 line 26
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1184 line 27
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1184 line 29
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1185 line 80
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1185 line 81
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1185 line 82
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1185 line 83
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1185 line 85
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1186 line 136
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1186 line 137
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1186 line 138
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1186 line 139
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1186 line 141
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1187 line 192
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1187 line 193
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1187 line 194
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1187 line 195
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1187 line 197
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1188 line 248
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1188 line 249
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1188 line 250
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1188 line 251
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1188 line 253
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1189 line 304
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1189 line 305
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1189 line 306
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1189 line 307
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1189 line 309
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1190 line 498
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1190 line 499
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1190 line 500
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1190 line 501
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1190 line 503
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1191 line 692
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1191 line 693
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1191 line 694
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1191 line 695
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1191 line 697
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1192 line 748
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1192 line 749
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1192 line 750
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1192 line 751
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1192 line 753
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1193 line 942
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1193 line 943
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1193 line 944
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1193 line 945
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1193 line 947
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1194 line 1136
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1194 line 1137
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1194 line 1138
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1194 line 1139
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1194 line 1141
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1195 line 1330
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1195 line 1331
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1195 line 1332
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1195 line 1333
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1195 line 1335
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1196 line 1386
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1196 line 1387
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1196 line 1388
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1196 line 1389
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1196 line 1391
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1197 line 1442
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1197 line 1443
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1197 line 1444
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1197 line 1445
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1197 line 1447
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1198 line 1498
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1198 line 1499
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1198 line 1500
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1198 line 1501
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1198 line 1503
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1199 line 1554
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1199 line 1555
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1199 line 1556
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1199 line 1557
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1199 line 1559
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1200 line 1748
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1200 line 1749
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1200 line 1750
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1200 line 1751
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1200 line 1753
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1201 line 1942
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1201 line 1943
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1201 line 1944
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1201 line 1945
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1201 line 1947
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1202 line 1998
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1202 line 1999
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1202 line 2000
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1202 line 2001
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1202 line 2003
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1203 line 2054
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1203 line 2055
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1203 line 2056
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1203 line 2057
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1203 line 2059
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1204 line 2110
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1204 line 2111
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1204 line 2112
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1204 line 2113
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1204 line 2115
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1205 line 2166
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1205 line 2167
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1205 line 2168
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1205 line 2169
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1205 line 2171
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1206 line 2222
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1206 line 2223
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1206 line 2224
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1206 line 2225
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1206 line 2227
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1207 line 2278
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1207 line 2279
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1207 line 2280
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1207 line 2281
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1207 line 2283
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1208 line 2334
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1208 line 2335
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1208 line 2336
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1208 line 2337
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1208 line 2339
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1209 line 2390
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1209 line 2391
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1209 line 2392
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1209 line 2393
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1209 line 2395
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1210 line 2446
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1210 line 2447
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1210 line 2448
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1210 line 2449
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1210 line 2451
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1211 line 2502
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1211 line 2503
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1211 line 2504
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1211 line 2505
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1211 line 2507
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1212 line 2558
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1212 line 2559
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1212 line 2560
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1212 line 2561
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1212 line 2563
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1213 line 2614
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1213 line 2615
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1213 line 2616
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1213 line 2617
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1213 line 2619
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1214 line 2670
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1214 line 2671
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1214 line 2672
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1214 line 2673
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1214 line 2675
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1215 line 2726
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1215 line 2727
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1215 line 2728
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1215 line 2729
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1215 line 2731