OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources75.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2400 line 50
2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2400 line 51
3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2400 line 52
4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2400 line 53
5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2400 line 55
6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2401 line 244
7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2401 line 245
8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2401 line 246
9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2401 line 247
10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2401 line 249
11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2402 line 438
12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2402 line 439
13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2402 line 440
14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2402 line 441
15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2402 line 443
16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2403 line 632
17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2403 line 633
18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2403 line 634
19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2403 line 635
20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2403 line 637
21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2404 line 826
22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2404 line 827
23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2404 line 828
24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2404 line 829
25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2404 line 831
26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2405 line 882
27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2405 line 883
28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2405 line 884
29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2405 line 885
30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2405 line 887
31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2406 line 1076
32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2406 line 1077
33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2406 line 1078
34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2406 line 1079
35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2406 line 1081
36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2407 line 1270
37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2407 line 1271
38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2407 line 1272
39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2407 line 1273
40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2407 line 1275
41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2408 line 1326
42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2408 line 1327
43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2408 line 1328
44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2408 line 1329
45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2408 line 1331
46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2409 line 1520
47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2409 line 1521
48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2409 line 1522
49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2409 line 1523
50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2409 line 1525
51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2410 line 1714
52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2410 line 1715
53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2410 line 1716
54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2410 line 1717
55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2410 line 1719
56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2411 line 1908
57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2411 line 1909
58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2411 line 1910
59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2411 line 1911
60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2411 line 1913
61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2412 line 2102
62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2412 line 2103
63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2412 line 2104
64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2412 line 2105
65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2412 line 2107
66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2413 line 2296
67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2413 line 2297
68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2413 line 2298
69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2413 line 2299
70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2413 line 2301
71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2414 line 2490
72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2414 line 2491
73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2414 line 2492
74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2414 line 2493
75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2414 line 2495
76. def OAI.MUB6.Certificate.MixedSemantics.sourceA2415 line 2684
77. def OAI.MUB6.Certificate.MixedSemantics.sourceB2415 line 2685
78. def OAI.MUB6.Certificate.MixedSemantics.sourceC2415 line 2686
79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2415 line 2687
80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2415 line 2689
81. def OAI.MUB6.Certificate.MixedSemantics.sourceA2416 line 2740
82. def OAI.MUB6.Certificate.MixedSemantics.sourceB2416 line 2741
83. def OAI.MUB6.Certificate.MixedSemantics.sourceC2416 line 2742
84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2416 line 2743
85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2416 line 2745
86. def OAI.MUB6.Certificate.MixedSemantics.sourceA2417 line 2934
87. def OAI.MUB6.Certificate.MixedSemantics.sourceB2417 line 2935
88. def OAI.MUB6.Certificate.MixedSemantics.sourceC2417 line 2936
89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2417 line 2937
90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2417 line 2939
91. def OAI.MUB6.Certificate.MixedSemantics.sourceA2418 line 3128
92. def OAI.MUB6.Certificate.MixedSemantics.sourceB2418 line 3129
93. def OAI.MUB6.Certificate.MixedSemantics.sourceC2418 line 3130
94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2418 line 3131
95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2418 line 3133
96. def OAI.MUB6.Certificate.MixedSemantics.sourceA2419 line 3322
97. def OAI.MUB6.Certificate.MixedSemantics.sourceB2419 line 3323
98. def OAI.MUB6.Certificate.MixedSemantics.sourceC2419 line 3324
99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2419 line 3325
100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2419 line 3327
101. def OAI.MUB6.Certificate.MixedSemantics.sourceA2420 line 3516
102. def OAI.MUB6.Certificate.MixedSemantics.sourceB2420 line 3517
103. def OAI.MUB6.Certificate.MixedSemantics.sourceC2420 line 3518
104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2420 line 3519
105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2420 line 3521
106. def OAI.MUB6.Certificate.MixedSemantics.sourceA2421 line 3710
107. def OAI.MUB6.Certificate.MixedSemantics.sourceB2421 line 3711
108. def OAI.MUB6.Certificate.MixedSemantics.sourceC2421 line 3712
109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2421 line 3713
110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2421 line 3715
111. def OAI.MUB6.Certificate.MixedSemantics.sourceA2422 line 3904
112. def OAI.MUB6.Certificate.MixedSemantics.sourceB2422 line 3905
113. def OAI.MUB6.Certificate.MixedSemantics.sourceC2422 line 3906
114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2422 line 3907
115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2422 line 3909
116. def OAI.MUB6.Certificate.MixedSemantics.sourceA2423 line 4098
117. def OAI.MUB6.Certificate.MixedSemantics.sourceB2423 line 4099
118. def OAI.MUB6.Certificate.MixedSemantics.sourceC2423 line 4100
119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2423 line 4101
120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2423 line 4103
121. def OAI.MUB6.Certificate.MixedSemantics.sourceA2424 line 4292
122. def OAI.MUB6.Certificate.MixedSemantics.sourceB2424 line 4293
123. def OAI.MUB6.Certificate.MixedSemantics.sourceC2424 line 4294
124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2424 line 4295
125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2424 line 4297
126. def OAI.MUB6.Certificate.MixedSemantics.sourceA2425 line 4486
127. def OAI.MUB6.Certificate.MixedSemantics.sourceB2425 line 4487
128. def OAI.MUB6.Certificate.MixedSemantics.sourceC2425 line 4488
129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2425 line 4489
130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2425 line 4491
131. def OAI.MUB6.Certificate.MixedSemantics.sourceA2426 line 4680
132. def OAI.MUB6.Certificate.MixedSemantics.sourceB2426 line 4681
133. def OAI.MUB6.Certificate.MixedSemantics.sourceC2426 line 4682
134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2426 line 4683
135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2426 line 4685
136. def OAI.MUB6.Certificate.MixedSemantics.sourceA2427 line 4874
137. def OAI.MUB6.Certificate.MixedSemantics.sourceB2427 line 4875
138. def OAI.MUB6.Certificate.MixedSemantics.sourceC2427 line 4876
139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2427 line 4877
140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2427 line 4879
141. def OAI.MUB6.Certificate.MixedSemantics.sourceA2428 line 5068
142. def OAI.MUB6.Certificate.MixedSemantics.sourceB2428 line 5069
143. def OAI.MUB6.Certificate.MixedSemantics.sourceC2428 line 5070
144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2428 line 5071
145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2428 line 5073
146. def OAI.MUB6.Certificate.MixedSemantics.sourceA2429 line 5262
147. def OAI.MUB6.Certificate.MixedSemantics.sourceB2429 line 5263
148. def OAI.MUB6.Certificate.MixedSemantics.sourceC2429 line 5264
149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2429 line 5265
150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2429 line 5267
151. def OAI.MUB6.Certificate.MixedSemantics.sourceA2430 line 5318
152. def OAI.MUB6.Certificate.MixedSemantics.sourceB2430 line 5319
153. def OAI.MUB6.Certificate.MixedSemantics.sourceC2430 line 5320
154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2430 line 5321
155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2430 line 5323
156. def OAI.MUB6.Certificate.MixedSemantics.sourceA2431 line 5374
157. def OAI.MUB6.Certificate.MixedSemantics.sourceB2431 line 5375
158. def OAI.MUB6.Certificate.MixedSemantics.sourceC2431 line 5376
159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2431 line 5377
160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2431 line 5379