OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources72.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2304 line 41
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2304 line 42
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2304 line 43
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2304 line 44
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2304 line 46
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2305 line 97
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2305 line 98
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2305 line 99
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2305 line 100
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2305 line 102
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2306 line 291
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2306 line 292
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2306 line 293
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2306 line 294
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2306 line 296
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2307 line 347
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2307 line 348
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2307 line 349
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2307 line 350
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2307 line 352
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2308 line 403
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2308 line 404
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2308 line 405
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2308 line 406
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2308 line 408
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2309 line 597
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2309 line 598
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2309 line 599
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2309 line 600
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2309 line 602
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2310 line 791
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2310 line 792
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2310 line 793
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2310 line 794
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2310 line 796
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2311 line 985
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2311 line 986
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2311 line 987
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2311 line 988
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2311 line 990
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2312 line 1179
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2312 line 1180
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2312 line 1181
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2312 line 1182
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2312 line 1184
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2313 line 1235
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2313 line 1236
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2313 line 1237
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2313 line 1238
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2313 line 1240
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2314 line 1291
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2314 line 1292
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2314 line 1293
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2314 line 1294
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2314 line 1296
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2315 line 1347
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2315 line 1348
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2315 line 1349
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2315 line 1350
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2315 line 1352
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2316 line 1403
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2316 line 1404
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2316 line 1405
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2316 line 1406
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2316 line 1408
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2317 line 1459
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2317 line 1460
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2317 line 1461
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2317 line 1462
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2317 line 1464
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2318 line 1515
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2318 line 1516
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2318 line 1517
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2318 line 1518
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2318 line 1520
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2319 line 1571
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2319 line 1572
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2319 line 1573
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2319 line 1574
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2319 line 1576
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2320 line 1627
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2320 line 1628
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2320 line 1629
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2320 line 1630
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2320 line 1632
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2321 line 1683
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2321 line 1684
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2321 line 1685
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2321 line 1686
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2321 line 1688
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2322 line 1739
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2322 line 1740
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2322 line 1741
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2322 line 1742
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2322 line 1744
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2323 line 1795
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2323 line 1796
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2323 line 1797
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2323 line 1798
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2323 line 1800
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2324 line 1851
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2324 line 1852
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2324 line 1853
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2324 line 1854
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2324 line 1856
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2325 line 1907
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2325 line 1908
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2325 line 1909
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2325 line 1910
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2325 line 1912
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2326 line 1963
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2326 line 1964
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2326 line 1965
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2326 line 1966
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2326 line 1968
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2327 line 2019
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2327 line 2020
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2327 line 2021
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2327 line 2022
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2327 line 2024
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2328 line 2075
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2328 line 2076
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2328 line 2077
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2328 line 2078
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2328 line 2080
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2329 line 2131
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2329 line 2132
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2329 line 2133
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2329 line 2134
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2329 line 2136
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2330 line 2187
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2330 line 2188
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2330 line 2189
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2330 line 2190
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2330 line 2192
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2331 line 2243
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2331 line 2244
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2331 line 2245
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2331 line 2246
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2331 line 2248
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2332 line 2299
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2332 line 2300
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2332 line 2301
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2332 line 2302
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2332 line 2304
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2333 line 2355
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2333 line 2356
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2333 line 2357
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2333 line 2358
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2333 line 2360
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2334 line 2411
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2334 line 2412
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2334 line 2413
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2334 line 2414
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2334 line 2416
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2335 line 2467
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2335 line 2468
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2335 line 2469
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2335 line 2470
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2335 line 2472