OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources74.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2368 line 45
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2368 line 46
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2368 line 47
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2368 line 48
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2368 line 50
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2369 line 101
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2369 line 102
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2369 line 103
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2369 line 104
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2369 line 106
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2370 line 295
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2370 line 296
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2370 line 297
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2370 line 298
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2370 line 300
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2371 line 351
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2371 line 352
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2371 line 353
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2371 line 354
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2371 line 356
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2372 line 407
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2372 line 408
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2372 line 409
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2372 line 410
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2372 line 412
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2373 line 463
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2373 line 464
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2373 line 465
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2373 line 466
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2373 line 468
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2374 line 519
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2374 line 520
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2374 line 521
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2374 line 522
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2374 line 524
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2375 line 575
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2375 line 576
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2375 line 577
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2375 line 578
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2375 line 580
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2376 line 631
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2376 line 632
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2376 line 633
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2376 line 634
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2376 line 636
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2377 line 687
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2377 line 688
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2377 line 689
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2377 line 690
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2377 line 692
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2378 line 743
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2378 line 744
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2378 line 745
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2378 line 746
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2378 line 748
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2379 line 799
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2379 line 800
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2379 line 801
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2379 line 802
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2379 line 804
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2380 line 855
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2380 line 856
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2380 line 857
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2380 line 858
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2380 line 860
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2381 line 1049
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2381 line 1050
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2381 line 1051
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2381 line 1052
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2381 line 1054
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2382 line 1243
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2382 line 1244
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2382 line 1245
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2382 line 1246
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2382 line 1248
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2383 line 1437
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2383 line 1438
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2383 line 1439
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2383 line 1440
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2383 line 1442
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2384 line 1631
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2384 line 1632
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2384 line 1633
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2384 line 1634
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2384 line 1636
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2385 line 1825
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2385 line 1826
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2385 line 1827
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2385 line 1828
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2385 line 1830
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2386 line 2019
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2386 line 2020
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2386 line 2021
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2386 line 2022
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2386 line 2024
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2387 line 2213
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2387 line 2214
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2387 line 2215
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2387 line 2216
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2387 line 2218
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2388 line 2407
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2388 line 2408
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2388 line 2409
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2388 line 2410
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2388 line 2412
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2389 line 2463
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2389 line 2464
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2389 line 2465
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2389 line 2466
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2389 line 2468
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2390 line 2519
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2390 line 2520
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2390 line 2521
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2390 line 2522
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2390 line 2524
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2391 line 2575
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2391 line 2576
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2391 line 2577
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2391 line 2578
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2391 line 2580
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2392 line 2769
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2392 line 2770
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2392 line 2771
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2392 line 2772
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2392 line 2774
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2393 line 2963
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2393 line 2964
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2393 line 2965
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2393 line 2966
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2393 line 2968
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2394 line 3019
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2394 line 3020
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2394 line 3021
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2394 line 3022
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2394 line 3024
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2395 line 3213
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2395 line 3214
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2395 line 3215
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2395 line 3216
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2395 line 3218
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2396 line 3407
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2396 line 3408
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2396 line 3409
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2396 line 3410
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2396 line 3412
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2397 line 3601
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2397 line 3602
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2397 line 3603
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2397 line 3604
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2397 line 3606
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2398 line 3795
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2398 line 3796
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2398 line 3797
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2398 line 3798
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2398 line 3800
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2399 line 3989
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2399 line 3990
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2399 line 3991
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2399 line 3992
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2399 line 3994