OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources77.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2464 line 45
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2464 line 46
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2464 line 47
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2464 line 48
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2464 line 50
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2465 line 239
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2465 line 240
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2465 line 241
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2465 line 242
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2465 line 244
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2466 line 433
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2466 line 434
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2466 line 435
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2466 line 436
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2466 line 438
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2467 line 627
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2467 line 628
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2467 line 629
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2467 line 630
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2467 line 632
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2468 line 821
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2468 line 822
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2468 line 823
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2468 line 824
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2468 line 826
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2469 line 1015
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2469 line 1016
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2469 line 1017
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2469 line 1018
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2469 line 1020
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2470 line 1071
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2470 line 1072
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2470 line 1073
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2470 line 1074
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2470 line 1076
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2471 line 1265
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2471 line 1266
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2471 line 1267
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2471 line 1268
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2471 line 1270
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2472 line 1459
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2472 line 1460
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2472 line 1461
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2472 line 1462
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2472 line 1464
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2473 line 1653
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2473 line 1654
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2473 line 1655
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2473 line 1656
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2473 line 1658
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2474 line 1847
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2474 line 1848
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2474 line 1849
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2474 line 1850
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2474 line 1852
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2475 line 2041
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2475 line 2042
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2475 line 2043
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2475 line 2044
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2475 line 2046
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2476 line 2235
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2476 line 2236
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2476 line 2237
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2476 line 2238
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2476 line 2240
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2477 line 2429
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2477 line 2430
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2477 line 2431
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2477 line 2432
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2477 line 2434
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2478 line 2623
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2478 line 2624
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2478 line 2625
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2478 line 2626
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2478 line 2628
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2479 line 2817
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2479 line 2818
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2479 line 2819
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2479 line 2820
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2479 line 2822
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2480 line 2873
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2480 line 2874
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2480 line 2875
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2480 line 2876
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2480 line 2878
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2481 line 3067
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2481 line 3068
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2481 line 3069
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2481 line 3070
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2481 line 3072
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2482 line 3261
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2482 line 3262
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2482 line 3263
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2482 line 3264
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2482 line 3266
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2483 line 3455
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2483 line 3456
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2483 line 3457
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2483 line 3458
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2483 line 3460
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2484 line 3649
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2484 line 3650
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2484 line 3651
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2484 line 3652
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2484 line 3654
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2485 line 3705
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2485 line 3706
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2485 line 3707
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2485 line 3708
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2485 line 3710
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2486 line 3899
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2486 line 3900
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2486 line 3901
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2486 line 3902
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2486 line 3904
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2487 line 4093
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2487 line 4094
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2487 line 4095
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2487 line 4096
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2487 line 4098
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2488 line 4287
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2488 line 4288
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2488 line 4289
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2488 line 4290
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2488 line 4292
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2489 line 4481
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2489 line 4482
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2489 line 4483
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2489 line 4484
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2489 line 4486
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2490 line 4675
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2490 line 4676
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2490 line 4677
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2490 line 4678
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2490 line 4680
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2491 line 4869
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2491 line 4870
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2491 line 4871
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2491 line 4872
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2491 line 4874
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2492 line 5063
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2492 line 5064
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2492 line 5065
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2492 line 5066
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2492 line 5068
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2493 line 5119
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2493 line 5120
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2493 line 5121
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2493 line 5122
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2493 line 5124
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2494 line 5175
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2494 line 5176
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2494 line 5177
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2494 line 5178
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2494 line 5180
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2495 line 5369
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2495 line 5370
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2495 line 5371
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2495 line 5372
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2495 line 5374