OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources71.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2272 line 40
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2272 line 41
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2272 line 42
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2272 line 43
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2272 line 45
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2273 line 96
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2273 line 97
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2273 line 98
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2273 line 99
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2273 line 101
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2274 line 290
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2274 line 291
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2274 line 292
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2274 line 293
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2274 line 295
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2275 line 484
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2275 line 485
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2275 line 486
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2275 line 487
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2275 line 489
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2276 line 678
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2276 line 679
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2276 line 680
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2276 line 681
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2276 line 683
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2277 line 734
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2277 line 735
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2277 line 736
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2277 line 737
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2277 line 739
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2278 line 790
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2278 line 791
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2278 line 792
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2278 line 793
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2278 line 795
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2279 line 846
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2279 line 847
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2279 line 848
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2279 line 849
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2279 line 851
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2280 line 1040
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2280 line 1041
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2280 line 1042
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2280 line 1043
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2280 line 1045
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2281 line 1234
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2281 line 1235
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2281 line 1236
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2281 line 1237
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2281 line 1239
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2282 line 1428
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2282 line 1429
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2282 line 1430
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2282 line 1431
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2282 line 1433
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2283 line 1622
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2283 line 1623
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2283 line 1624
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2283 line 1625
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2283 line 1627
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2284 line 1816
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2284 line 1817
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2284 line 1818
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2284 line 1819
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2284 line 1821
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2285 line 2010
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2285 line 2011
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2285 line 2012
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2285 line 2013
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2285 line 2015
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2286 line 2204
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2286 line 2205
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2286 line 2206
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2286 line 2207
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2286 line 2209
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2287 line 2260
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2287 line 2261
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2287 line 2262
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2287 line 2263
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2287 line 2265
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2288 line 2316
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2288 line 2317
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2288 line 2318
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2288 line 2319
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2288 line 2321
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2289 line 2372
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2289 line 2373
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2289 line 2374
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2289 line 2375
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2289 line 2377
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2290 line 2566
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2290 line 2567
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2290 line 2568
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2290 line 2569
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2290 line 2571
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2291 line 2760
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2291 line 2761
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2291 line 2762
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2291 line 2763
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2291 line 2765
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2292 line 2954
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2292 line 2955
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2292 line 2956
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2292 line 2957
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2292 line 2959
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2293 line 3010
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2293 line 3011
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2293 line 3012
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2293 line 3013
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2293 line 3015
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2294 line 3066
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2294 line 3067
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2294 line 3068
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2294 line 3069
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2294 line 3071
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2295 line 3122
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2295 line 3123
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2295 line 3124
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2295 line 3125
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2295 line 3127
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2296 line 3316
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2296 line 3317
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2296 line 3318
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2296 line 3319
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2296 line 3321
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2297 line 3510
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2297 line 3511
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2297 line 3512
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2297 line 3513
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2297 line 3515
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2298 line 3704
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2298 line 3705
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2298 line 3706
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2298 line 3707
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2298 line 3709
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2299 line 3760
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2299 line 3761
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2299 line 3762
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2299 line 3763
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2299 line 3765
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2300 line 3816
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2300 line 3817
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2300 line 3818
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2300 line 3819
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2300 line 3821
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2301 line 4010
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2301 line 4011
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2301 line 4012
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2301 line 4013
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2301 line 4015
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2302 line 4204
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2302 line 4205
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2302 line 4206
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2302 line 4207
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2302 line 4209
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2303 line 4398
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2303 line 4399
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2303 line 4400
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2303 line 4401
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2303 line 4403