OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources36.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1152 line 21
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1152 line 22
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1152 line 23
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1152 line 24
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1152 line 26
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1153 line 77
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1153 line 78
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1153 line 79
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1153 line 80
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1153 line 82
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1154 line 133
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1154 line 134
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1154 line 135
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1154 line 136
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1154 line 138
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1155 line 189
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1155 line 190
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1155 line 191
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1155 line 192
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1155 line 194
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1156 line 245
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1156 line 246
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1156 line 247
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1156 line 248
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1156 line 250
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1157 line 301
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1157 line 302
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1157 line 303
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1157 line 304
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1157 line 306
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1158 line 357
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1158 line 358
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1158 line 359
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1158 line 360
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1158 line 362
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1159 line 413
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1159 line 414
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1159 line 415
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1159 line 416
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1159 line 418
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1160 line 607
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1160 line 608
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1160 line 609
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1160 line 610
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1160 line 612
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1161 line 801
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1161 line 802
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1161 line 803
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1161 line 804
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1161 line 806
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1162 line 995
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1162 line 996
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1162 line 997
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1162 line 998
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1162 line 1000
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1163 line 1189
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1163 line 1190
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1163 line 1191
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1163 line 1192
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1163 line 1194
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1164 line 1245
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1164 line 1246
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1164 line 1247
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1164 line 1248
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1164 line 1250
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1165 line 1439
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1165 line 1440
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1165 line 1441
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1165 line 1442
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1165 line 1444
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1166 line 1633
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1166 line 1634
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1166 line 1635
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1166 line 1636
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1166 line 1638
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1167 line 1827
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1167 line 1828
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1167 line 1829
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1167 line 1830
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1167 line 1832
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1168 line 1883
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1168 line 1884
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1168 line 1885
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1168 line 1886
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1168 line 1888
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1169 line 1939
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1169 line 1940
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1169 line 1941
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1169 line 1942
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1169 line 1944
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1170 line 1995
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1170 line 1996
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1170 line 1997
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1170 line 1998
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1170 line 2000
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1171 line 2051
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1171 line 2052
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1171 line 2053
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1171 line 2054
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1171 line 2056
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1172 line 2107
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1172 line 2108
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1172 line 2109
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1172 line 2110
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1172 line 2112
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1173 line 2301
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1173 line 2302
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1173 line 2303
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1173 line 2304
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1173 line 2306
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1174 line 2495
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1174 line 2496
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1174 line 2497
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1174 line 2498
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1174 line 2500
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1175 line 2689
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1175 line 2690
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1175 line 2691
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1175 line 2692
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1175 line 2694
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1176 line 2883
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1176 line 2884
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1176 line 2885
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1176 line 2886
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1176 line 2888
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1177 line 3077
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1177 line 3078
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1177 line 3079
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1177 line 3080
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1177 line 3082
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1178 line 3133
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1178 line 3134
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1178 line 3135
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1178 line 3136
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1178 line 3138
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1179 line 3189
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1179 line 3190
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1179 line 3191
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1179 line 3192
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1179 line 3194
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1180 line 3245
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1180 line 3246
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1180 line 3247
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1180 line 3248
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1180 line 3250
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1181 line 3301
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1181 line 3302
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1181 line 3303
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1181 line 3304
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1181 line 3306
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1182 line 3357
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1182 line 3358
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1182 line 3359
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1182 line 3360
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1182 line 3362
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1183 line 3413
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1183 line 3414
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1183 line 3415
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1183 line 3416
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1183 line 3418