OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources68.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2176 line 35
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2176 line 36
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2176 line 37
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2176 line 38
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2176 line 40
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2177 line 91
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2177 line 92
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2177 line 93
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2177 line 94
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2177 line 96
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2178 line 147
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2178 line 148
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2178 line 149
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2178 line 150
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2178 line 152
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2179 line 341
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2179 line 342
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2179 line 343
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2179 line 344
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2179 line 346
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2180 line 535
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2180 line 536
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2180 line 537
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2180 line 538
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2180 line 540
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2181 line 729
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2181 line 730
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2181 line 731
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2181 line 732
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2181 line 734
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2182 line 923
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2182 line 924
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2182 line 925
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2182 line 926
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2182 line 928
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2183 line 979
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2183 line 980
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2183 line 981
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2183 line 982
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2183 line 984
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2184 line 1173
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2184 line 1174
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2184 line 1175
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2184 line 1176
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2184 line 1178
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2185 line 1229
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2185 line 1230
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2185 line 1231
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2185 line 1232
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2185 line 1234
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2186 line 1285
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2186 line 1286
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2186 line 1287
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2186 line 1288
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2186 line 1290
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2187 line 1341
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2187 line 1342
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2187 line 1343
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2187 line 1344
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2187 line 1346
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2188 line 1397
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2188 line 1398
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2188 line 1399
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2188 line 1400
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2188 line 1402
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2189 line 1453
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2189 line 1454
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2189 line 1455
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2189 line 1456
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2189 line 1458
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2190 line 1509
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2190 line 1510
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2190 line 1511
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2190 line 1512
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2190 line 1514
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2191 line 1703
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2191 line 1704
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2191 line 1705
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2191 line 1706
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2191 line 1708
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2192 line 1897
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2192 line 1898
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2192 line 1899
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2192 line 1900
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2192 line 1902
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2193 line 2091
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2193 line 2092
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2193 line 2093
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2193 line 2094
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2193 line 2096
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2194 line 2147
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2194 line 2148
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2194 line 2149
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2194 line 2150
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2194 line 2152
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2195 line 2203
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2195 line 2204
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2195 line 2205
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2195 line 2206
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2195 line 2208
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2196 line 2259
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2196 line 2260
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2196 line 2261
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2196 line 2262
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2196 line 2264
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2197 line 2315
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2197 line 2316
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2197 line 2317
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2197 line 2318
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2197 line 2320
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2198 line 2509
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2198 line 2510
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2198 line 2511
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2198 line 2512
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2198 line 2514
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2199 line 2703
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2199 line 2704
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2199 line 2705
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2199 line 2706
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2199 line 2708
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2200 line 2897
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2200 line 2898
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2200 line 2899
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2200 line 2900
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2200 line 2902
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2201 line 2953
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2201 line 2954
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2201 line 2955
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2201 line 2956
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2201 line 2958
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2202 line 3009
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2202 line 3010
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2202 line 3011
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2202 line 3012
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2202 line 3014
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2203 line 3065
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2203 line 3066
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2203 line 3067
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2203 line 3068
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2203 line 3070
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2204 line 3121
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2204 line 3122
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2204 line 3123
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2204 line 3124
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2204 line 3126
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2205 line 3177
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2205 line 3178
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2205 line 3179
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2205 line 3180
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2205 line 3182
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2206 line 3233
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2206 line 3234
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2206 line 3235
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2206 line 3236
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2206 line 3238
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2207 line 3289
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2207 line 3290
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2207 line 3291
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2207 line 3292
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2207 line 3294