OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources73.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2336 line 71
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2336 line 72
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2336 line 73
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2336 line 74
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2336 line 76
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2337 line 127
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2337 line 128
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2337 line 129
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2337 line 130
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2337 line 132
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2338 line 183
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2338 line 184
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2338 line 185
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2338 line 186
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2338 line 188
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2339 line 377
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2339 line 378
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2339 line 379
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2339 line 380
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2339 line 382
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2340 line 571
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2340 line 572
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2340 line 573
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2340 line 574
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2340 line 576
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2341 line 765
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2341 line 766
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2341 line 767
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2341 line 768
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2341 line 770
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2342 line 959
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2342 line 960
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2342 line 961
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2342 line 962
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2342 line 964
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2343 line 1153
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2343 line 1154
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2343 line 1155
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2343 line 1156
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2343 line 1158
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2344 line 1347
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2344 line 1348
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2344 line 1349
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2344 line 1350
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2344 line 1352
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2345 line 1541
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2345 line 1542
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2345 line 1543
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2345 line 1544
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2345 line 1546
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2346 line 1735
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2346 line 1736
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2346 line 1737
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2346 line 1738
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2346 line 1740
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2347 line 1929
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2347 line 1930
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2347 line 1931
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2347 line 1932
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2347 line 1934
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2348 line 2123
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2348 line 2124
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2348 line 2125
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2348 line 2126
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2348 line 2128
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2349 line 2317
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2349 line 2318
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2349 line 2319
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2349 line 2320
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2349 line 2322
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2350 line 2511
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2350 line 2512
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2350 line 2513
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2350 line 2514
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2350 line 2516
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2351 line 2705
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2351 line 2706
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2351 line 2707
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2351 line 2708
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2351 line 2710
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2352 line 2899
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2352 line 2900
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2352 line 2901
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2352 line 2902
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2352 line 2904
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2353 line 3093
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2353 line 3094
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2353 line 3095
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2353 line 3096
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2353 line 3098
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2354 line 3287
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2354 line 3288
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2354 line 3289
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2354 line 3290
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2354 line 3292
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2355 line 3481
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2355 line 3482
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2355 line 3483
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2355 line 3484
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2355 line 3486
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2356 line 3537
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2356 line 3538
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2356 line 3539
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2356 line 3540
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2356 line 3542
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2357 line 3593
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2357 line 3594
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2357 line 3595
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2357 line 3596
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2357 line 3598
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2358 line 3649
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2358 line 3650
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2358 line 3651
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2358 line 3652
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2358 line 3654
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2359 line 3705
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2359 line 3706
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2359 line 3707
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2359 line 3708
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2359 line 3710
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2360 line 3761
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2360 line 3762
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2360 line 3763
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2360 line 3764
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2360 line 3766
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2361 line 3955
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2361 line 3956
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2361 line 3957
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2361 line 3958
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2361 line 3960
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2362 line 4149
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2362 line 4150
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2362 line 4151
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2362 line 4152
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2362 line 4154
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2363 line 4343
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2363 line 4344
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2363 line 4345
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2363 line 4346
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2363 line 4348
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2364 line 4537
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2364 line 4538
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2364 line 4539
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2364 line 4540
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2364 line 4542
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2365 line 4731
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2365 line 4732
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2365 line 4733
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2365 line 4734
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2365 line 4736
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2366 line 4925
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2366 line 4926
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2366 line 4927
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2366 line 4928
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2366 line 4930
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2367 line 5119
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2367 line 5120
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2367 line 5121
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2367 line 5122
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2367 line 5124